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

Re: [PVS-Help] Change theorem name



Francisco,

The old proof became a orphaned proof. Use the command M-x
show-orphaned-proof to display a list of orphaned proofs. Select the old
proof with the letter s. Go to your new lemma and install the proof (M-x
install-proof).

There is no an easy way to rename a lemma or definition. But this is
"the stardard" way:

* Write a theory top.pvs that imports all your theories.
* Dump the file top.pvs including imported theories in a file top.dmp.
* Edit the file top.dmp and replace the old name with the new name. Be
careful, not to replace instances of the old name that you actually
want.
* Undump the file.
* Type check and prove top.dmp to be sure that everything works.

Cesar

On Tue, 2005-02-01 at 10:16, Francisco Jose CHAVES ALONSO wrote:
> If by mistake I change a theorem name how can I recover the prove?
> 
> How can I change a theorem name without losting the prove?
> 
> There is any emacs command for change the theorem name?
> 
-- 
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace      mailto://C.A.Munoz@larc.nasa.gov
144 Research Drive                  http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 766 1539 Fax +1 (757) 766 1855