Thanks for the advice. That worked perfectly. I will keep that in mind for
I appreciate the assistance.
13/14 UC IEEE President
PhD Candidate - EE Systems
University of Cincinnati
On Thu, Jun 19, 2014 at 3:29 PM, Rob Arthan <r...@lemma-one.com> wrote:
> 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.
> On 19 Jun 2014, at 17:59, Jon Lockhart <jal...@bucknell.edu> 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@lemma-one.com
> > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Proofpower mailing list