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
If you need other theories in scope, add them as parents e.g.
Proofpower mailing list