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.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

Reply via email to