ACL2-pc::ACL2-wrap
(macro) same as (lisp x)
Example:
(acl2-wrap (pe :here))
General Form:
(acl2-wrap form)
Same as (lisp form). This is provided for interface tools that want
to be able to execute the same form in raw Lisp, in the proof-builder, or in
the ACL2 top-level loop (lp).
