LP, the Larch Prover -- The qed command
The qed command constitutes a claim that all proofs are finished.
<qed-command> ::= qed
The qed command checks that the proof stack is empty. If it is not, LP
prints an error message and halts execution of all .lp