[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: How to recover from a runaway proof attempt?

> I have encountered problems when trying to recover after a proof attempt
> gone wrong (various reasons, eg rewriting depth going wild :-)

This is described on page 6 of the Prover Guide:

Interrupting Proofs:  The proof checker can be interrupted when it is
working on a command by typing C-c C-c.  This places the system at a
Lisp break.  Typing (restore) at the break returns the system to the
Rule? prompt corresponding to the last interaction.


Dr Dave Stringer-Calvert, Software Engineer, Computer Science Laboratory,
SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, USA.
Phone: (650) 859-3291    Fax: (650) 859-2844   Email: dave_sc@csl.sri.com