Define an alias for a documentation topic.
(defpointer acl2s acl2-sedan) (defpointer guard-hints xargs t)
(defpointer new-topic target-topic [keyword-p])
A common practice when documenting keyword symbols is to create a
doc topic in in the "ACL2" package or some other relevant package,
rather than the "KEYWORD" package to which the keyword symbol
rightfully belongs. In keeping with this practice, the