Retrieve named theory
For direct evaluation at the top-level loop:
(let ((world (w state))) (theory 'ground-zero))
In the examples above, the theory returned is the one in force when ACL2 is started up (see ground-zero).
General Form: (theory name)
This ``function'' is actually a macro that expands to a term mentioning the
single free variable world. When theory expressions are evaluated by
in-theory or the