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" <phil.clay...@lineone.net> 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 Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
