		Search-engine friendly clone of the ACL2 documentation.

@url

Construct an XDOC tree for a mangled topic link directive @(url ...).

Macro: @url

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

Function: @url-fn

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

Theorem: stringp-of-@url

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