Phil,

After resetting the command window and rerunning the commands today, I was
able to run my specification to the point where I was running into the
exception with no problems. I must of somehow changed the proof context I
guess, though the print status was coming up that is was ok. Not sure, but
it was probably on my typing in a command wrong.

Thanks for the help. I am sure I will be back with more questions today as
I try to prove portions of my specification.

Regards,
Jon


On Sun, Sep 2, 2012 at 9:00 PM, Phil Clayton <phil.clay...@lineone.net>wrote:

> 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" <phil.clay...@lineone.net
>> <mailto:phil.clayton@lineone.**net <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<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