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

Re: [PVS-Help] Change theorem name

>If by mistake I change a theorem name how can I recover the prove?

Use M-x show-orphaned-proofs to find your old proof.  You
can the use M-x edit-proof to insert the proof  back into
your theorem with the new name. (i.e. C-c C-c)

>How can I change a theorem name without losting the prove?
>There is any emacs command for change the theorem name?

The way I change a theorem name is as follows:
      (1)  Use M-x edit-proof to capture proof, save it in Emacs
             kill ring  (e.g. C-w OR M-w)
      (2)  Rename proof
      (3)  M-x tc
      (4)  M-x edit-proof and "paste" proof into buffer
      (5) C-c C-c

Rick Butler