MAKE-THEORY : MEXPRMAKE-THEORY is a top-level command.
Create a new theory. A theory is defined by (optionally) starting
from an old theory, and adding rewrite rules and axioms. You can also attach
other library objects to the theory, which will then be loaded with it.
This will also make an abbreviation of the same name.
All of the objects in the theory should be defined in the library.
The command format for MAKE-THEORY is:
<n>MAKE-THEORY NAME EXTENDS AXIOMS RRULES OTHER MHELP
"SYMBOL" "SYMBOLLIST" "SYMBOLLIST" "SYMBOLLIST" "SYMBOLLIST" "STRING"
The arguments have the following meaning:
NAME : Name of new theory
EXTENDS : Theories which this theory extends.
AXIOMS : Axioms
RRULES : Rewrite rules
OTHER : Other library objects
MHELP : Help message
TPS documentation homepage