LP, the Larch Prover -- The delete command

The delete command discards facts from LP's logical system.

Syntax

<delete-command> ::= delete <names>

Examples

delete rewrite-rules
delete myLemma, junk

Usage

The delete command deletes the named facts from the system. It can be used to get rid of unhelpful facts (e.g., unorderable or unnecessary critical-pair equations) or facts that have served their purpose and are no longer needed.