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
name is the name of a previously executed deftheory event
(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 :in-theory hint, world is bound to the
current ACL2 world.
