		Search-engine friendly clone of the ACL2 documentation.

@``

Construct an XDOC tree for an evaluation 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)))