Jon, Change “Z” on the first line of your Z paragraph to “ZAX” and all should be well. Spivey Z, ProofPower-Z and ISO Z all require this bit of mark-up to distinguish axiomatic descriptions with the predicate part omitted (what you want) and given set definitions, free type definitions and constraints. The typesetting in ProofPower-Z is not quite in line with Spivey Z and ISO Z, because it gives you independent control of whether to print the vertical bar on the left, whereas I think the presence or absence of the vertical bar is intended to be a visual clue to what kind of paragraph you have in Spivey Z and ISO Z.
Regards, Rob. On 19 Jun 2014, at 17:59, Jon Lockhart <[email protected]> wrote: > Dear All, > > I am throwing an odd exception recently when working on a small example > specification. In checking the manuals and Z books there seems to be no > reason that this exception is being thrown. It is even used in the vending > machine example in the Z Tutorial book. I have attached the exact piece that > is giving me the exception and the output from ProofPower. > > If anyone has any ideas on what might be causing it, please let me know. > > Regards, > Jon Lockhart > PhD Candidate > EE Systems > University of Cincinnati > <simpleError.doc>_______________________________________________ > 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
