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. 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.