		Search-engine friendly clone of the ACL2 documentation.

@body

Construct an XDOC tree for a body directive @(body ...).

Macro: @body

(defmacro @body (&rest trees)
  (list '@body-fn (cons 'list trees)))

Function: @body-fn

(defun @body-fn (trees)
  (declare (xargs :guard (tree-listp trees)))
  (make-tree-dir/&& :@body trees))

Theorem: stringp-of-@body

(defthm stringp-of-@body
  (equal (treep (@body-fn trees))
         (tree-listp trees)))