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

Reply via email to