		Search-engine friendly clone of the ACL2 documentation.

@tsee

Construct an XDOC tree for a typewriter topic link directive @(tsee ...).

Macro: @tsee

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

Function: @tsee-fn

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

Theorem: stringp-of-@tsee

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