LP, the Larch Prover -- The define-class command

The define-class command introduces an abbreviation for a set of named facts. This abbreviation can be used wherever <names> are required as an argument to a command.


<define-class-command> ::= define-class <class-name> [ <names> ]


define-class $facts nat, set
define-class $facts1 copy($facts)
define-class $old eval(*)


The define-class command defines <class-name> as an abbreviation for <names>. If no <names> are specified, the command prints the current definition of <class-name>. The examples define the following abbreviations: See also <name>.