Rob, Thanks for the advice. That worked perfectly. I will keep that in mind for the future.
I appreciate the assistance. Regards, Jon Regards, 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 <[email protected]> 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 <[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
