Hi John,
That sounds strange. It's probably easiest if you can cut your example
down to a short script that produces the error, say containing just a
single paragraph, and send a zipped version of that to the list.
Phil
On 03/09/12 01:47, Jon Lockhart wrote:
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" <[email protected]
<mailto:[email protected]>> 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
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
