retrieve named theory
Major Section:  THEORIES

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