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

About orphaned-proofs.prf

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:p.s.miner@larc.nasa.gov
-- Hampton, Virginia 23681-2199 | http://shemesh.larc.nasa.gov/~psm/