On Saturday 25 Aug 2012 20:47, Jon Lockhart wrote: > I did have a question on some of the outputs from the > tutorial document. Currently I am on user013C and when I > have placed some of the commands into the terminal, via > the execute line command, the ProofPower output is not > the same as is reported in the document. Is this due to > some changes that have been made since this document was > published in 2002? Also a few of the rewrite commands > that were in the document threw exceptions.
On my system usr013A-C all load OK (in fact if they didn't the build would have failed since I think they are loaded in creating the examples database). That is to say, if you start with a clean HOL database and do docsml on each of usr013A-C and then load file on each, they go through fine. So the possible reasons for your failures are: 1. You are starting with the wrong database or 2. you are copy and pasting something for which some prior script is essential but has not been executed. or 3. you are trying to execute something which is in the document for explanation but is not there to be executed in that context. (e.g. something in a "GFT" section rather than an "SML" section). If you can't figure it out from that then you will need to post exactly what you have done and what the result was. Roger Jones _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com