[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Jei-Wen Teng writes:
> Did anyone know how to install one of the orphaned proofs in the file
> "orphaned-proofs.prf"? I do not know how to retrieve back one of the
> orphaned proofs in that file. Many thanks.
M-x show-orphaned-proofs will produce a buffer that lists all the
proofs in orphaned-proofs.prf. Position the cursor on the proof you
want to reclaim (in the Formula column). If you then type "s", pvs
will open a Proof buffer with the selected proof.
See pp 25-28 in the PVS System Guide.
-- Paul S. Miner | phone: (757) 864-6201
-- 1 South Wright St. / MS 130 | fax: (757) 864-4234
-- NASA Langley Research Center | mailto:email@example.com
-- Hampton, Virginia 23681-2199 | http://shemesh.larc.nasa.gov/~psm/