Build a description of the
Macro:
(defmacro xdoc::desc-apt-input-old (&rest additional) (cons 'xdoc::desc (cons '"@('old')" (cons '(xdoc::p "Denotes the target function to transform.") (cons '(xdoc::p "It must be the name of a function, or a <see topic='@(url acl2::numbered-names)'>numbered name</see> with a wildcard index that <see topic='@(url acl2::resolve-numbered-name-wildcard)'>resolves</see> to the name of a function. In the rest of this documentation page, for expository convenience, it is assumed that @('old') is the name of the denoted function.") additional)))))