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.
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.
> On 03/09/12 01:47, Jon Lockhart wrote:
>> 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?
>> 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
>> in my specification. More specifically I am trying to and a
>> 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
>> 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
Proofpower mailing list