LP, the Larch Prover — The make command
The make command changes the activity or immunity of
a collection of facts or of the current conjecture.
<make_command> ::= make <fact-status> ( <names> | conjecture )
<fact-status> ::= active | passive | immune | nonimmune | ancestor-immune
Note: The <fact-status> can be abbreviated.
Examples
make inactive rewrite-rules
make immune conjecture
Usage
LP automatically uses any rewrite rules made active by the make command to
normalize terms appearing in the current conjecture or in nonimmune facts in
LP's logical system. It also automatically applies any deduction rules made
active by the make command.
LP automatically normalizes any rewrite rules and deduction rules made
nonimmune by the make command, and it applies all active deduction rules
to these deimmunized rules.
See the activity and immunity settings.