next up previous contents
Next: Special Declarations Up: The Theory Environment Previous: The Syntax Lists

Declarations and Comments

Constants and operators can be declared using the declareconstant, declareinfix (declares flat operators), and declaretypedinfix (declares operators with nontrivial type) commands.

Constants and operators can also be declared implicitly via the declaration and proof commands. It should be noted that theorem names are constants of a theory! When constants are defined, the name of the defining theorem is the same as the name of the object being defined; when operators are defined, the name of the defining theorem must be given as a parameter.

A single declaration can be viewed using the showdec command. A declaration line contains the identifier followed by the left and right types (both 0 in the case of non-operators) and the default left argument if there is one. The showalldecs or scandecs commands can be used to view all declarations.

Declarations now also include comments. New comments (superseding any previous comments) can be attached to a declared object using the newcomment command; the appendcomment command appends comments to any previously existing comments. showdec and thmdisplay (and all derived commands) display comments.

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