		Search-engine friendly clone of the ACL2 documentation.

@''

Construct an XDOC tree for a inline code directive @('...').

Macro: @''

(defmacro |@''| (&rest trees)
  (list '|@''-FN| (cons 'list trees)))

Function: @''-fn

(defun |@''-FN| (trees)
  (declare (xargs :guard (tree-listp trees)))
  (make-tree-dir/&& :|@''| trees))

Theorem: stringp-of-@''

(defthm |STRINGP-OF-@''|
  (equal (treep (|@''-FN| trees))
         (tree-listp trees)))