Jon,

Can you post the actual input that is failing, please. (To protect it in 
transit, either gzip your .doc file and attach it to your post, or use 
conv_ascii to convert it into ASCII).

Regards,

Rob.

Regards,

Rob.

On 3 Sep 2012, at 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" <phil.clay...@lineone.net> 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
> Proofpower@lemma-one.com
> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to