Currently enabled rules as of logical name
Examples: (current-theory :here) (current-theory 'lemma3)
General Form: (current-theory logical-name)
Returns the current theory as it existed immediately after the introduction
of logical-name provided it is evaluated in an environment in which
the variable symbol WORLD is bound to the current ACL2 logical world,
ACL2 !>(current-theory :here)
will cause an (unbound variable) error while
ACL2 !>(let ((world (w state))) (current-theory :here))
will return the current theory in world.
See theories and see logical-name for a discussion of
theories in general and why the commonly used ``theory functions'' such as
You may experience a fencepost problem in deciding which logical name to use. Deflabel can always be used to mark unambiguously for future reference a particular point in the development of your theory. The order of events in the vicinity of an encapsulate is confusing. See encapsulate.
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