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.

Syntax

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

Examples

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

Usage

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:

$facts is an abbreviation for nat, set. The command display $facts is equivalent to the command display nat, set.
$facts1 is also an abbreviation for nat, set. Without the copy operation, it would be an abbreviation for $facts, whose meaning would change if $facts was redefined.
$old is an abbreviation for the list of names of all facts in LP's logical system when the define-class command was executed; the eval operation forces the evaluation of its argument *. The command display $old displays the current forms of any of those facts that are still in LP's logical system when the display command is executed.