Phil, Ok, let me try to restart and reload the system and see if that corrects it. If not then i will do as you say and send it out.
You guys may have it though. I am currently using Anthony's example that came with ZWordTools bc it is simple and great for trying to get a handle on the tools. Thanks, Jon On Sep 2, 2012 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
