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
