THEORY

retrieve named theory 
Major Section:  THEORIES


Example:
(theory 'my-theory)


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.