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

Re: PVS proofs in batch mode



Cesar A. Munoz writes:
   From: "Cesar A. Munoz" <munoz@nianet.org>
   Date: 19 Nov 2003 14:23:05 -0500
   Subject: PVS proofs in batch mode
   
   Hi,
   
   Is there a way to associate script proofs to lemmas in batch mode ?
   
If you generate the pvs files then you can also generate the prf
files. Thats what I use for the CCSL compiler. 

For the format of the prf files see the "Format of the .prf
files" thread on this mailing list:
http://pvs.csl.sri.com/mail-archive/pvs/msg01036.html

Bye,

Hendrik