Major Section: THEORIES
Example: (theory 'ground-zero)In the example above, the theory returned is the one in force when ACL2 is started up (see ground-zero).
General Form: (theory name)where
nameis the name of a previously executed
deftheoryevent (otherwise a hard error occurs). Returns the named theory. See theories.
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
world is bound to the
current ACL2 world.