Major Section: THEORIES
Examples: (executable-counterpart-theory :here) (executable-counterpart-theory 'lemma3)See logical-name.
General Form: (executable-counterpart-theory logical-name)Returns the theory containing all the
:executable-counterpart
runes, whether enabled or not, that existed immediately after
logical-name was introduced. See the documentation for
theories, logical-name, executable-counterpart and
function-theory.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 :in-theory hint, world is bound to
the current ACL2 world.
