|
|
|---|
|
|
|
|---|
Functions for obtaining or producing theories
Example Calls of Theory Functions: (universal-theory :here) (union-theories th1 th2) (set-difference-theories th1 th2)
The theory functions are documented individually:
The functions (actually, macros) mentioned above are convenient ways to produce theories. (See theories.) Some, like universal-theory, take a logical name (see logical-name) as an argument and return the relevant theory as of the time that name was introduced. Others, like union-theories, take two theories and produce a new one. See redundant-events for a caution about the use of logical names in theory expressions.
Theory expressions are generally composed of applications of theory
functions. Formally, theory expressions are expressions that involve, at
most, the free variable world and that when evaluated with world bound to the current ACL2 world (see world) return theories. The ``theory functions'' are actually macros that expand into
forms that involve the free variable world. Thus, for example