On 13 Aug 2012, at 13:31, Jon Lockhart wrote: > Rob, > > Ok so looks like I am looking to rewrite all my specifications again in > ProofPower. A minor inconvenience but should not be a problem.
That is likely the quickest way to get started. > I will just pop up my specs on one screen and bring up ProofPower's XPP up on > the other screen in my Linux VM, and I should be able to rewrite them with no > problems. The only thing I can't seem to find is the symbol library in XPP. I > have found where I can insert the various Zed structures, no problem, but > there is supposed to be an XPP keyboard that has these symbols, based on the > pictures in the documentation. Is this available in the editor version of XPP > or do I need to run the full version of XPP to have access to that? > The keyboard in the picture is the actual keyboard, although you may need to do a bit more work to set it up. There is a tool called the Palette in the Tools menu that lets you enter all the symbols with mouse clicks without having to do any more set-up and without having to learn the key combinations. If you do want to set up the keyboard have a read of section 4.3 of the Xpp manual and the comments at the head of the file app-defaults/XppKeyboard in the first instance. > Once I get these in the system though, I definitely need to get some proofs > written for them. That is where I am having a fair bit of trouble with the > examples and documentation at the moment. I have a solid grasp of Z, and from > Rogers email and the documentation, I can just write the proofs mostly in Z, > which would save me some time in having to learn HOL right now, though I > think I will learn it anyways for the future, just at a slower pace. In any > case, the proof writing is not the issue, it is the writing in the ProofPower > environment I guess I am hung up on, along with a few other minor things. > > I will look over all the documentation again on the site Rob, and continuing > to see if I can get the examples operational so I can apply what is shown > there to my open specifications. Good luck! And do keep asking if you have any more problems. Regards, Rob. _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com