Phil, After resetting the command window and rerunning the commands today, I was able to run my specification to the point where I was running into the exception with no problems. I must of somehow changed the proof context I guess, though the print status was coming up that is was ok. Not sure, but it was probably on my typing in a command wrong.
Thanks for the help. I am sure I will be back with more questions today as I try to prove portions of my specification. Regards, Jon On Sun, Sep 2, 2012 at 9:00 PM, Phil Clayton <[email protected]>wrote: > Hi John, > > That sounds strange. It's probably easiest if you can cut your example > down to a short script that produces the error, say containing just a > single paragraph, and send a zipped version of that to the list. > > Phil > > > > On 03/09/12 01:47, Jon Lockhart wrote: > >> Phil, >> >> Thanks for the reply. I have set it so up like that where the parent >> theory is z_library and my new theory is named something else. Just ran >> the print status again and that is what it says as well. >> >> Could it be one more minor thing is not loaded? >> >> Regards, >> Jon >> >> On Sep 2, 2012 8:43 PM, "Phil Clayton" <[email protected] >> <mailto:phil.clayton@lineone.**net <[email protected]>>> wrote: >> >> Hi John, >> >> On 02/09/12 23:59, Jon Lockhart wrote: >> >> The problem I am having is this. I am trying to use the union >> operator >> in my specification. More specifically I am trying to and a >> individual >> item to a set in the predicate of a specification paragraph in >> z, which >> is allowed by the rules of the language. The PP system comes >> back with >> expection 62000 of the Z-Parser, saying that the union symbol >> from the >> palette is a free variable and those are not permitted in Z >> paragraphs. >> >> >> If ProofPower says that ∪ is a variable then the Z toolkit theory >> "z_sets" that defines the Z global variable (_ ∪ _) is not in scope, >> i.e. "z_sets" is not an ancestor theory of your current theory. >> >> Generally, Z specifications should always have the theory >> "z_library" as an ancestor, which brings all Z toolkit theories into >> scope. Typically your theory would start >> >> open_theory "z_library"; >> new_theory "some_new_theory"; >> ... >> >> If you need other theories in scope, add them as parents e.g. >> >> new_parent "z_reals"; >> >> Phil >> >> >> >> ______________________________**_________________ >> Proofpower mailing list >> [email protected] >> http://lemma-one.com/mailman/**listinfo/proofpower_lemma-one.**com<http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com> >> >> >
_______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
