THEORY

retrieve named theory
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.