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

*To*: pvs-help@csl.sri.com*Subject*: Help - using PVS*From*: Kong Woei Susanto <susanto@dcs.gla.ac.uk>*Date*: Thu, 22 Jul 1999 16:08:27 +0000*Sender*: susanto@dcs.gla.ac.uk

Hi, 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 file exploded. each proof can take > 200K. 2. Is there any primitive proof command to expand a definition without simplification ? 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 minutes. 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) thanks, -- Kong Woei Susanto Department of Computing Science - University of Glasgow 17 Lilybank Gardens, Glasgow G12 8RZ, Scotland, United Kingdom. e-mail: susanto@dcs.gla.ac.uk Ph: +44-141-3304454 fax:+44-141-3304913

- Prev by Date:
**Recursive Functions with negative domain** - Next by Date:
**User libraries in the PVS lib directory** - Prev by thread:
**Re: User libraries in the PVS lib directory** - Next by thread:
**Re: Help - using PVS** - Index(es):