Executable-counterpart rules as of logical name
Examples: (executable-counterpart-theory :here) (executable-counterpart-theory 'lemma3)
General Form: (executable-counterpart-theory logical-name)
Returns the theory containing all the
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