		Search-engine friendly clone of the ACL2 documentation.

@csym

Construct an XDOC tree for a capitalized printed topic link directive @(csym ...).

Macro: @csym

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

Function: @csym-fn

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

Theorem: stringp-of-@csym

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