next up previous contents
Next: Theorems Up: The Theory Environment Previous: Declarations and Comments

Special Declarations

The declarepretheorem command is used to indicate the intent of proving a theorem with a given name (this can be an operator).

The declareopaque and declarenotopaque commands can be used to enter and remove operators from the opacity list. Free variable operators can be declared opaque to block them from being declared with types. New restriction: declareopaque can now be used only to declare an operator initially; it is still possible to use declarenotopaque to remove opacity, but this is irreversible.

The makescin and makescout commands declare infixes or functions as having input or output (resp.) restricted to absolute types (strongly Cantorian sets). The user must supply a witnessing theorem. These declarations allow the stratification restrictions on terms involving these infixes to be weakened appropriately, without the use of explicit type retractions.

The proveprogram command can be used to bind a theorem to a constant or operator as a ``functional program''. The theorem must have a suitable form (the left side must be a substitution instance of a term which would be admissable as the left side of a definition of the constant or operator). The deprogram command removes the binding. The seeprogram (for one constant or operator) or seeallprograms commands can be used to view information about this list.

The forget command will eliminate declarations of theorems depending on or referring to a given theorem.

The definition commands are described above. A single definition can be viewed using the seedef command (it takes the name of the defined object as parameter and displays the defining theorem); all definitions can be seen using the seealldefs command.



Randall Holmes
Fri Sep 5 16:28:58 MDT 1997