LP, the Larch Prover -- The delete command

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


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


delete rewrite-rules
delete myLemma, junk


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.