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

Reply via email to