		Search-engine friendly clone of the ACL2 documentation.

Executable-counterpart-theory

Executable-counterpart rules as of logical name

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.