|
|
|---|
|
|
|
|---|
Retrieve named theory
Examples:
For use in in-theory events or
(theory 'ground-zero)
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)
where
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