Jon, Can you post the actual input that is failing, please. (To protect it in transit, either gzip your .doc file and attach it to your post, or use conv_ascii to convert it into ASCII).
Regards, Rob. Regards, Rob. On 3 Sep 2012, at 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]> 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
_______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
