Hello Community, I was wondering if I could get some help with trying to start to write up proofs for some Zed specifications I have already written.
I have read the documentation on the site, and tried playing with the examples provided, but I am still have a fair amount of difficulty. Rather than flounder around, I figure I ask for help. I have already written the specifications in Word using Z Word Tools, and they are already saved in a variety of formats. I have them transferred over to my linux image. What format do they need to be in for me to get to import them into XPP so I can begin the proof development. My second question is once you get those specifications into XPP and the ProofPower tools, then how do you start writing the proofs on the Zed specs? Is it supposed to be in Zed terminology or in HOL? Any help would appreciated in getting things rolling. Thanks, Jon Lockhart
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
