Jon, You are right that Rob is the man to answer your technical problem, but in the meantime I might be able to help you round it.
"save_and_quit();" is something that I never use. If your system otherwise seems OK then you should go right ahead and work through the tutorial. Why don't I use it? Well, whenever I am working interactively with ProofPower I just don't save the database. I always have a make system in the background ready to build in batch mode, and this uses proofpower with the "-f" option to run a script and then save it. So when I have a working script I create a new database using "make". This must be possible with your system otherwise you would not have completed the build of ProofPower. When I resume work on an incomplete development I will enter the current document with xpp picking the database with all prior documents loaded, and then I use "use_file" to run the current script through to the point of failure where I was last working (and I force failure by just putting "stop;" in the script at the point I am working). Then I continue my interactive work. When I have a clean document I save it and then do a make to create a new database. You probably don't want to set up a makefile for working through the tutorial, but you can still work in a similar manner, i.e. instead of saving the database when you pause in the tutorial, just put "stop here;" in your script, save it, and quit xpp. When you come back use "use_file" to run your script through to your current position in the tutorial. (you will need to use docsml on the file first if it is not pure SML, but for the tutorial you can just work with an SML script). I presume you are looking at usr004, which is the gentlest introduction to ProofPower-HOL. Alternatively you could work through the ProofPower HOL course usr022 with its accompanying tutorial notes usr013, which is less gentle but I think, more systematic and has greater coverage (but doesn't actually mention "save_and_quit()") Roger Jones _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
