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


2. you are copy and pasting something for which some prior 
script is essential but has not been executed.


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" 

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

Reply via email to