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