| Auxiliary-Item = [ then ] Statement | Private-Definition . | |
| Canceled-Theorem = canceled [ Numeral ] ; . | |
| Private-Definition = | |
| Constant-Definition | | |
| Private-Functor-Definition | | |
| Private-Predicate-Definition . | |
| Constant-Definition = set Equating-List ; . | |
| Equating-List = Equating { , Equating } . | |
| Equating = Variable-Identifier = Term-Expression . | |
Last modified: June 26, 2000