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";


Proofpower mailing list

Reply via email to