Thanks for the advice. That worked perfectly. I will keep that in mind for
the future.

I appreciate the assistance.


Jon Lockhart
13/14 UC IEEE President
PhD Candidate - EE Systems
University of Cincinnati

On Thu, Jun 19, 2014 at 3:29 PM, Rob Arthan <> wrote:

> 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 <> 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
> >
> >
Proofpower mailing list

Reply via email to