[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Help - using PVS
1. Is there any possibility to disable pretty-printing on the
proof(.prf) file ?
I have to prove some lemmas, in which each of them had a long proof
sequence (> 300 commands). Because of the preety printing, the proof
exploded. each proof can take > 200K.
2. Is there any primitive proof command to expand a definition without
3. In the middle of my proof, I wanted to expand a definition.
Somehow, the command (ex: (expand "x")) took a very long time > 10
Is it because of simplification ? Any suggestion on what should I do
(If it's needed, I have a dump file for the lemma. The file size is
around 1.2 M)
fyi: My system is running on LINUX - PII 400 - 256M(RAM)
Kong Woei Susanto
Department of Computing Science - University of Glasgow
17 Lilybank Gardens, Glasgow G12 8RZ, Scotland, United Kingdom.
e-mail: email@example.com Ph: +44-141-3304454 fax:+44-141-3304913