		Search-engine friendly clone of the ACL2 documentation.

@csee

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

Macro: @csee

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

Function: @csee-fn

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

Theorem: stringp-of-@csee

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