%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% oz.sty
%
\message{`OZ Macros' <9 Nov 90>}
%
%	This document is organised as follows:
%
%	SECTION 1	Z FONTS
%	SECTION 2	Z SYMBOLS
%	SECTION 3	Z ENVIRONMENTS
%
% Modification History:
%
%               The original zed.sty file was written by Mike Spivey.
%               These macros have been extensively modified to
%               include extra symbols and environments for Object-Z
%               and now have little resemblence to the original macros.
%               Mike Spivey has also extended his macros along
%               different lines for Z - the latest version of macros
%               are called fuzz.sty and come with a syntax checker for Z.
%               They can be purchased for a small fee from:
%                       mike@prg.oxford.ac.uk
%
%        87	original zed.sty file - Mike Spivey
%        88	modified to include extra symbols and environments - Paul King
%        88	modified to include macros for UQ editor - Ray Neucom
%    May 89	modified to include object-oriented constructs - PK
%    Jun 89	modified to automatically change Z symbol size - PK
% 27 Jul 89	removed spurious space from \@setsize - PK
%  3 Aug 89	adjust style of equation number field - PK
% 24 Aug 89     add optional field to topline and zedline for proofs - PK
% 15 Sep 89     added extra qed symbols, updated classcom and comment - PK
% 25 Sep 89	renamed z@[bB]ig to z[bB]ig and changed temporal symbols - PK
% 30 Sep 89	added \znewpage, \Infrule, removed space above state box - PK
% 12 Mar 90	changed \@setsize to work better for double-spaced text - PK
% 31 Mar 90	added definition for @ and \bool and redefined `;' - PK
%  9 May 90	changed \sdef to \varsdef, \sdef & \defs to Spivey's latest - PK
% 27 May 90	added \c{n}{text} - a tab like \t{n} with text at left - PK
% 29 May 90	added `corners' to boxes and \zedcornerheight - PK
% 11 Jul 90	added \rename*[y/x] and \zseq \zset ..., changed \zeq \zimp - PK
%  2 Aug 90     added subseq - PK
%  9 Nov 90	changed \M to hopefully interact better with spacing - PK
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Please post any updates that you may make to this file to:
%	Paul King -- ACSnet: king@batserver.cs.uq.oz.au
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%	SECTION 1	Z FONTS
%
% The AMS extra symbol fonts are loaded.
%	Note: msxm and msym sometimes called euxm and euym respectively
%       NOTE: the new AMSFONTS 2.0 call these fonts msam and msbm repectively
%       (the fonts below need to be renamed if you want to use the new fonts)
%
\font\fivmsx=msxm5			\font\fivmsy=msym5
\font\sixmsx=msxm6			\font\sixmsy=msym6
\font\sevmsx=msxm7			\font\sevmsy=msym7
\font\egtmsx=msxm8			\font\egtmsy=msym8
\font\ninmsx=msxm9			\font\ninmsy=msym9
\font\tenmsx=msxm10			\font\tenmsy=msym10
\font\elvmsx=msxm10 \@halfmag		\font\elvmsy=msym10 \@halfmag
\font\twlmsx=msxm10 \@magscale1		\font\twlmsy=msym10 \@magscale1
\font\frtnmsx=msxm10 \@magscale2	\font\frtnmsy=msym10 \@magscale2
\font\svtnmsx=msxm10 \@magscale3	\font\svtnmsy=msym10 \@magscale3
\font\twtymsx=msxm10 \@magscale4	\font\twtymsy=msym10 \@magscale4
\font\twfvmsx=msxm10 \@magscale5	\font\twfvmsy=msym10 \@magscale5

%
% Load fonts not normally loaded
%
\font\frtnit=cmti10\@magscale2
\font\svtnit=cmti10\@magscale3
\font\twtyit=cmti10\@magscale4
\font\twfvit=cmti10\@magscale5
\font\twfvsy=cmsy10\@magscale5
\font\twtybf=cmbx10\@magscale4
\font\twfvbf=cmbx10\@magscale5

\newfam\msxfam
\newfam\msyfam

%
% Now make size changing commands automatically change size of Z symbols
% Doesn't work for letters in the cmex fonts e.g. \bigcup, \sum
%
\def\@vpt{\textfont\msxfam=\fivmsx
	\textfont\msyfam=\fivmsy}
%
\def\@vipt{\textfont\msxfam=\sixmsx
	\textfont\msyfam=\sixmsy}
%
\def\@viipt{\textfont\msxfam=\sevmsx
	\textfont\msyfam=\sevmsy}
%
\def\@viiipt{\textfont\msxfam=\egtmsx
	\textfont\msyfam=\egtmsy}
%
\def\@ixpt{\textfont\msxfam=\ninmsx \scriptfont\msxfam=\sixmsx
	\textfont\msyfam=\ninmsy \scriptfont\msyfam=\sixmsy}
%
\def\@xpt{\textfont\msxfam=\tenmsx \scriptfont\msxfam=\sevmsx
	\textfont\msyfam=\tenmsy \scriptfont\msyfam=\sevmsy}
%
\def\@xipt{\textfont\msxfam=\elvmsx \scriptfont\msxfam=\egtmsx
	\textfont\msyfam=\elvmsy \scriptfont\msyfam=\egtmsy}
%
\def\@xiipt{\textfont\msxfam=\twlmsx \scriptfont\msxfam=\ninmsx
	\textfont\msyfam=\twlmsy \scriptfont\msyfam=\ninmsy}
%
\def\@xivpt{\textfont\msxfam=\frtnmsx \scriptfont\msxfam=\tenmsx
	\textfont\msyfam=\frtnmsy \scriptfont\msyfam=\tenmsy
	\textfont\itfam=\frtnit \scriptfont\itfam=\tenit}
%
\def\@xviipt{\textfont\msxfam=\svtnmsx \scriptfont\msxfam=\twlmsx
	\textfont\msyfam=\svtnmsy \scriptfont\msyfam=\twlmsy
	\textfont\itfam=\svtnit \scriptfont\itfam=\twlit}
%
\def\@xxpt{\textfont\msxfam=\twtymsx \scriptfont\msxfam=\frtnmsx
	\textfont\msyfam=\twtymsy \scriptfont\msyfam=\frtnmsy
	\textfont\bffam=\twtybf
	\textfont\itfam=\twtyit \scriptfont\itfam=\frtnit}
%
\def\@xxvpt{\textfont\msxfam=\twfvmsx \scriptfont\msxfam=\svtnmsx
	\textfont\msyfam=\twfvmsy \scriptfont\msyfam=\svtnmsy
	\textfont\itfam=\twtyit \scriptfont\itfam=\svtnit
	\textfont\bffam=\twfvbf \scriptfont\tw@=\svtnsy}
%

\def\bbold{\fam\msyfam}
\def\@famletter#1{\ifcase #1 0\or 1\or 2\or 3\or 4\or 5\or 6\or 7\or
	8\or 9\or A\or B\or C\or D\or E\or F\fi}

\edef\@fx{\@famletter\msxfam}
\edef\@fy{\@famletter\msyfam}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%	SECTION 2	Z SYMBOLS
%
% The mathcodes for the letters A, ..., Z, a, ..., z are changed to
% generate text italic rather than math italic by default. This makes
% multi-letter identifiers look better. The mathcode for character c
% is set to "7000 (variable family) + "400 (text italic) + c.
%

\def\@setmcodes#1#2#3{{\count0=#1 \count1=#3
	\loop \global\mathcode\count0=\count1 \ifnum \count0<#2
	\advance\count0 by1 \advance\count1 by1 \repeat}}

\@setmcodes{`A}{`Z}{"7441}
\@setmcodes{`a}{`z}{"7461}
%
% Also, the mathcode for semicolon is set to "8000, so it behaves as an
% active character in math mode; it is defined to insert a thick space.
% \semicolon is a semicolon as an ordinary symbol.
%
\let\@mc=\mathchardef
\mathcode`\;="8000 % Makes ; active in math mode
{\catcode`\;=\active \gdef;{\semicolon\;}}
\@mc\semicolon="603B

%
%		------ UTILITY MACROS FOR Z SYMBOLS ------
%

% \z@op		makes a large math operator
% \z@rel	makes a math relation
% \z@bin	makes a binary operator
%
% each use a mathstrut to defeat TeX's vertical adjustment.
% \z@bigXXX big version of symbol
%
\def\z@op#1{\mathop{\mathstrut{#1}}\nolimits}
\def\z@bin#1{\mathbin{\mathstrut{#1}}}
\def\z@rel#1{\mathrel{\mathstrut{#1}}}
%
\def\z@bigop#1{\z@op{\zbig{#1}}}
\def\z@bigbin#1{\z@bin{\zbig{#1}}}
\def\z@bigrel#1{\z@rel{\zbig{#1}}}
%
\def\z@Bigop#1{\z@op{\zBig{#1}}}
\def\z@Bigbin#1{\z@bin{\zBig{#1}}}
\def\z@Bigrel#1{\z@rel{\zBig{#1}}}
%
\def\z@smallop#1{\z@op{\zsmall{#1}}}
\def\z@smallbin#1{\z@bin{\zsmall{#1}}}
\def\z@smallrel#1{\z@rel{\zsmall{#1}}}
%
% This underscore doesn't have the little kern --- you get an italic
% correction anyway in math mode.
\def\_{\leavevmode \vbox{\hrule width0.4em}}

% Save \q as \xq for quantifiers q.
\let\xforall=\forall
\let\xexists=\exists
\let\xlambda=\lambda
\let\xmu=\mu
% Save other symbols
\let\xsucc\succ
\let\xprec\prec
\let\dotaccent=\dot
\let\sectionsymbol=\S
\let\integral=\int
\let\product\prod

% \p and \f make arrows with 1 and 2 crossings resp.
\def\p#1{\mathrel{\ooalign{\hfil$\mapstochar\mkern 5mu$\hfil\cr$#1$}}}
\def\f#1{\mathrel{\ooalign{\hfil
	$\mapstochar\mkern 3mu\mapstochar\mkern 5mu$\hfil\cr$#1$}}}
%
%	------ AMSTEX SYMBOL DEFINITIONS ------
%
% do these before Z symbols so that we can use them in our special symbols
%
%	msxm font
%
\@mc \boxdot	"2\@fx00
\@mc \boxplus	"2\@fx01
\@mc \boxtimes	"2\@fx02
\@mc \square      "0\@fx03
\@mc \blacksquare	"0\@fx04
\@mc \centerdot	"2\@fx05
\@mc \lozenge	"0\@fx06
\@mc \blacklozenge	"0\@fx07
\@mc \circlearrowright	"3\@fx08
\@mc \circlearrowleft	"3\@fx09
\@mc \rightleftharpoons	"3\@fx0A
\@mc \leftrightharpoons	"3\@fx0B
\@mc \boxminus	"2\@fx0C
\@mc \Vdash	"3\@fx0D
\@mc \Vvdash	"3\@fx0E
\@mc \vDash	"3\@fx0F
\@mc \twoheadrightarrow	"3\@fx10
\@mc \twoheadleftarrow	"3\@fx11
\@mc \leftleftarrows	"3\@fx12
\@mc \rightrightarrows	"3\@fx13
\@mc \upuparrows	"3\@fx14
\@mc \downdownarrows	"3\@fx15
\@mc \upharpoonright	"3\@fx16
\let \restriction	\upharpoonright
\@mc \downharpoonright	"3\@fx17
\@mc \upharpoonleft	"3\@fx18
\@mc \downharpoonleft	"3\@fx19
\@mc \rightarrowtail	"3\@fx1A
\@mc \leftarrowtail	"3\@fx1B
\@mc \leftrightarrows	"3\@fx1C
\@mc \rightleftarrows	"3\@fx1D
\@mc \Lsh	"3\@fx1E
\@mc \Rsh	"3\@fx1F
\@mc \rightsquigarrow	"3\@fx20
\@mc \leftrightsquigarrow	"3\@fx21
\@mc \looparrowleft	"3\@fx22
\@mc \looparrowright	"3\@fx23
\@mc \circeq	"3\@fx24
\@mc \succsim	"3\@fx25
\@mc \gtrsim	"3\@fx26
\@mc \gtrapprox	"3\@fx27
\@mc \multimap	"3\@fx28
\@mc \therefore	"3\@fx29
\@mc \because	"3\@fx2A
\@mc \doteqdot	"3\@fx2B
\let \Doteq	\doteqdot
\@mc \triangleq	"3\@fx2C
\@mc \precsim	"3\@fx2D
\@mc \lesssim	"3\@fx2E
\@mc \lessapprox	"3\@fx2F
\@mc \eqslantless	"3\@fx30
\@mc \eqslantgtr	"3\@fx31
\@mc \curlyeqprec	"3\@fx32
\@mc \curlyeqsucc	"3\@fx33
\@mc \preccurlyeq	"3\@fx34
\@mc \leqq	"3\@fx35
\@mc \leqslant  "3\@fx36
\@mc \lessgtr	"3\@fx37
\@mc \backprime	"0\@fx38
\@mc \risingdotseq	"3\@fx3A
\@mc \fallingdotseq	"3\@fx3B
\@mc \succcurlyeq	"3\@fx3C
\@mc \geqq	"3\@fx3D
\@mc \geqslant  "3\@fx3E
\@mc \gtrless	"3\@fx3F
\@mc \sqsubset	"3\@fx40
\@mc \sqsupset	"3\@fx41
\@mc \vartriangleright	"3\@fx42
\@mc \vartriangleleft	"3\@fx43
\@mc \trianglerighteq	"3\@fx44
\@mc \trianglelefteq	"3\@fx45
\@mc \bigstar	"0\@fx46
\@mc \between	"3\@fx47
\@mc \blacktriangledown	"0\@fx48
\@mc \blacktriangleright	"3\@fx49
\@mc \blacktriangleleft	"3\@fx4A
\@mc \vartriangle	"0\@fx4D
\@mc \blacktriangle	"0\@fx4E
\@mc \triangledown	"0\@fx4F
\@mc \eqcirc	"3\@fx50
\@mc \lesseqgtr	"3\@fx51
\@mc \gtreqless	"3\@fx52
\@mc \lesseqqgtr	"3\@fx53
\@mc \gtreqqless	"3\@fx54
\def \yen	{\mathhexbox\@fx55 }
\@mc \Rrightarrow	"3\@fx56
\@mc \Lleftarrow	"3\@fx57
\def \checkmark	{\mathhexbox\@fx58 }
\@mc \veebar	"2\@fx59
\@mc \barwedge	"2\@fx5A
\@mc \doublebarwedge	"2\@fx5B
\@mc \angle	"0\@fx5C
\@mc \measuredangle	"0\@fx5D
\@mc \sphericalangle	"0\@fx5E
\@mc \varpropto	"3\@fx5F
\@mc \smallsmile	"3\@fx60
\@mc \smallfrown	"3\@fx61
\@mc \Subset	"3\@fx62
\@mc \Supset	"3\@fx63
\@mc \Cup	"2\@fx64
\let \doublecup	\Cup
\@mc \Cap	"2\@fx65
\let \doublecap	\Cap
\@mc \curlywedge	"2\@fx66
\@mc \curlyvee	"2\@fx67
\@mc \leftthreetimes	"2\@fx68
\@mc \rightthreetimes	"2\@fx69
\@mc \subseteqq	"3\@fx6A
\@mc \supseteqq	"3\@fx6B
\@mc \bumpeq	"3\@fx6C
\@mc \Bumpeq	"3\@fx6D
\@mc \lll	"3\@fx6E
\let \llless	\lll
\@mc \ggg	"3\@fx6F
\let \gggtr	\ggg
\def \ulcorner	{\delimiter"4\@fx70\@fx70 }
\def \urcorner	{\delimiter"5\@fx71\@fx71 }
\def \circledR	{\mathhexbox\@fx72 }
\@mc \circledS	"0\@fx73
\@mc \pitchfork	"3\@fx74
\@mc \dotplus	"2\@fx75
\@mc \backsim	"3\@fx76
\@mc \backsimeq	"3\@fx77
\def \llcorner	{\delimiter"4\@fx78\@fx78 }
\def \lrcorner	{\delimiter"5\@fx79\@fx79 }
\def \maltese	{\mathhexbox\@fx7A }
\@mc \complement	"0\@fx7B
\@mc \intercal	"2\@fx7C
\@mc \circledcirc	"2\@fx7D
\@mc \circledast	"2\@fx7E
\@mc \circleddash	"2\@fx7F
%
%	msym font
%
\@mc \lvertneqq "3\@fy00
\@mc \gvertneqq "3\@fy01
\@mc \nleq	"3\@fy02
\@mc \ngeq	"3\@fy03
\@mc \nless	"3\@fy04
\@mc \ngtr	"3\@fy05
\@mc \nprec	"3\@fy06
\@mc \nsucc	"3\@fy07
\@mc \lneqq	"3\@fy08
\@mc \gneqq	"3\@fy09
\@mc \nleqslant	"3\@fy0A
\@mc \ngeqslant	"3\@fy0B
\@mc \lneq	"3\@fy0C
\@mc \gneq	"3\@fy0D
\@mc \npreceq	"3\@fy0E
\@mc \nsucceq	"3\@fy0F
\@mc \precnsim	"3\@fy10
\@mc \succnsim	"3\@fy11
\@mc \lnsim	"3\@fy12
\@mc \gnsim	"3\@fy13
\@mc \nleqq	"3\@fy14
\@mc \ngeqq	"3\@fy15
\@mc \precneqq	"3\@fy16
\@mc \succneqq	"3\@fy17
\@mc \precnapprox	"3\@fy18
\@mc \succnapprox	"3\@fy19
\@mc \lnapprox	"3\@fy1A
\@mc \gnapprox	"3\@fy1B
\@mc \nsim	"3\@fy1C
\@mc \ncong	"3\@fy1D
\def \napprox	{\not\approx}
%\@mc \varsubsetneq "3\@fy20
%\@mc \varsupsetneq "3\@fy21
\@mc \nsubseteqq	"3\@fy22
\@mc \nsupseteqq	"3\@fy23
\@mc \subsetneqq	"3\@fy24
\@mc \supsetneqq	"3\@fy25
%\@mc \varsubsetneqq	"3\@fy26
%\@mc \varsupsetneqq	"3\@fy27
\@mc \subsetneq	"3\@fy28
\@mc \supsetneq	"3\@fy29
\@mc \nsubseteq	"3\@fy2A
\@mc \nsupseteq	"3\@fy2B
\@mc \nparallel	"3\@fy2C
\@mc \nmid	"3\@fy2D
\@mc \nshortmid	"3\@fy2E
\@mc \nshortparallel	"3\@fy2F
\@mc \nvdash	"3\@fy30
\@mc \nVdash	"3\@fy31
\@mc \nvDash	"3\@fy32
\@mc \nVDash	"3\@fy33
\@mc \ntrianglerighteq	"3\@fy34
\@mc \ntrianglelefteq	"3\@fy35
\@mc \ntriangleleft	"3\@fy36
\@mc \ntriangleright	"3\@fy37
\@mc \nleftarrow	"3\@fy38
\@mc \nrightarrow	"3\@fy39
\@mc \nLeftarrow	"3\@fy3A
\@mc \nRightarrow	"3\@fy3B
\@mc \nLeftrightarrow	"3\@fy3C
\@mc \nleftrightarrow	"3\@fy3D
\@mc \divideontimes	"2\@fy3E
\@mc \varnothing	"0\@fy3F
\@mc \mho	"0\@fy66
\@mc \eth	"0\@fy67
\@mc \eqsim	"3\@fy68
\@mc \beth	"0\@fy69
\@mc \gimel	"0\@fy6A
\@mc \daleth	"0\@fy6B
\@mc \lessdot	"3\@fy6C
\@mc \gtrdot	"3\@fy6D
\@mc \ltimes	"2\@fy6E
\@mc \rtimes	"2\@fy6F
\@mc \shortmid	"3\@fy70
\@mc \shortparallel	"3\@fy71
\def \interleave	{{\parallel\!\!\vert}}
\def \shortinterleave	{\z@rel{\mathord\shortmid\mathord\shortparallel}}
\@mc \smallsetminus	"2\@fy72
\@mc \thicksim	"3\@fy73
\@mc \thickapprox	"3\@fy74
\@mc \approxeq	"3\@fy75
\@mc \succapprox	"3\@fy76
\@mc \precapprox	"3\@fy77
\@mc \curvearrowleft	"3\@fy78
\@mc \curvearrowright	"3\@fy79
\@mc \digamma	"0\@fy7A
\@mc \varkappa	"0\@fy7B
\@mc \hslash	"0\@fy7D
\@mc \hbar	"0\@fy7E
\@mc \backepsilon	"3\@fy7F
%
%		------ SPECIAL Z SYMBOLS ------
%
%	NUMBERS
%
\def \nat	{{\bbold N}}
\def \integer	{{\bbold Z}}
\def \natone	{{\bbold N}_1}
\def \real	{{\bbold R}}
\def \bool	{{\bbold B}}
\let \divides	\div
\def \div	{\z@bin{\rm div}}
\def \mod	{\z@bin{\rm mod}}
\def \succ	{\word{succ}}
\def \expon	{^}
%	aliases
\let \num	\integer
\let \nplus	\natone
%
%	LOGIC
%
\def \lnot	{\neg\;}
\def \land	{\z@rel{\wedge}}
\def \lor	{\z@rel{\vee}}
\let \imp	\Rightarrow
\let \iff	\Leftrightarrow
\def \all	{\z@op{\xforall}}
\def \exi	{\z@op{\xexists}}
\def \exione	{\exists_1}
\@mc \nexi	"0\@fy40
\def \dot	{\z@rel{\bullet}}
\def \true	{\keyword{true}}
\def \false	{\keyword{false}}
\let \cond	\rightarrow
%	aliases
\let \spot	\dot
\mathcode`\@="8000% make @ active in mathmode
{\catcode`\@=\active \gdef@{\dot}}
\let \implies	\imp
\let \forall	\all
\let \exists	\exi
\let \nexists	\nexi
%
%	SETS
%
\let \emptyset  \varnothing
\def \varemptyset  {\{\,\}}
\def \pset	{\z@op{\bbold P}}
\def \psetone	{\pset_1}
\def \fset	{\z@op{\bbold F}}
\def \fsetone	{\fset_1}
\def \sset	{\z@op{\bbold S}}
\let \mem	\in
\def \nem	{\not\mem}
\def \uni	{\z@bin\cup}
\def \int	{\z@bin\cap}
\let \prod	\times
\def \min	{\word{min}}
\def \max	{\word{max}}
\def \duni	{\z@Bigop{\lower0.25ex\hbox{$\uni$}}}
\def \dint	{\z@Bigop{\lower0.25ex\hbox{$\int$}}}
\def \upto	{\z@bin{\ldotp\ldotp}}
\let \psubs	\subset
\let \subs	\subseteq
\let \psups	\supset
\let \sups	\supseteq
\def \diff	{\z@bin{\backslash}}
%	aliases
\let \cross	\prod
\let \notin	\nem
\let \nmem	\nem
\let \union	\uni
\let \inter	\int
\let \power	\pset
\let \finset	\fset
\let \dunion	\duni
\let \dinter	\dint
%
%	RELATIONS & FUNCTIONS
%
\def \lambda	{\z@op{\xlambda}}
\def \mu	{\z@op{\xmu}}
\def \dom	{\keyword{dom}}
\def \ran	{\keyword{ran}}
\def \id	{\keyword{id}}
\@mc \dres	"2\@fx43
\@mc \rres	"2\@fx42
\def \dsub	{\mathbin{\rlap{\raise.05ex\hbox{$-$}}{\dres}}}
\def \rsub	{\mathbin{\rlap{\raise.05ex\hbox{$-$}}{\rres}}}
\let \fovr	\oplus
\let \cmp	\circ
\def \fcmp	{\mathbin{\raise 0.6ex\hbox{\oalign{\hfil$\scriptscriptstyle
		 \rm o$\hfil\cr\hfil$\scriptscriptstyle\rm 9$\hfil}}}}
\def \inv	{^{-1}}
\def \limg	{(\!|}
\def \rimg	{|\!)}
\let \map	\mapsto
\let \rel	\leftrightarrow
\let \tfun	\rightarrow
\let \tinj	\rightarrowtail
\def \tsur	{\mathrel{\ooalign{$\tfun$\hfil\cr$\mkern4mu\tfun$}}}
\def \pfun	{\p\tfun}
\def \pinj	{\p\tinj}
\def \psur	{\p\tsur}
\def \ffun	{\f\tfun}
\def \finj	{\f\tinj}
\def \bij	{\mathrel{\ooalign{$\tinj$\hfil\cr$\mkern5mu\tfun$}}}
\def \tcl	{^+}
\def \rtcl	{^*}
\def \iter	{^}
%	aliases
\let \comp	\fcmp
\let \ndres	\dsub
\let \nrres	\rsub
\let \fun	\tfun
\let \inj	\tinj
\let \surj	\tsur
\let \psurj	\psur
%
%	SEQUENCES
%
\def \seq	{\keyword{seq}}
\def \seqone	{\seq_1}
\def \emptyseq  {\lseq\,\rseq}
\let \lseq	\langle
\let \rseq	\rangle
\def \head	{\word{head}}
\def \tail	{\word{tail}}
\def \front	{\word{front}}
\def \last	{\word{last}}
\def \rev	{\word{rev}}
\def \squash	{\word{squash}}
\def \next	{\keyword{next}}
\def \inseq	{\keyword{in}}
\def \cat	{\mathbin{\raise 0.8ex\hbox{$\mathchar"2\@fx61$}}}
\@mc \sres	"2\@fx16
\def \ssub	{\z@bin{\rlap{$-$}{\sres}}}
\@mc \ires	"2\@fx18
\def \isub	{\z@bin{\rlap{$-$}{\ires}}}
\def \dcat	{\z@op{\cat/}}
\def \dovr	{\z@op{\fovr/}}
\def \dcmp	{\z@op{\fcmp/}}
\let \prefix	\subseteq
\def \suffix	{\keyword{suffix}}
\def \seqi	{\keyword{seq_\infty}}
\def \partitions	{\keyword{partitions}}
\def \disjoint	{\keyword{disjoint}}
\def \subseq	{\keyword{subseq}}
%	aliases
\let \filter	\sres
%
%	SCHEMAS
%
\def \lsch	{\z@bigop{\hbox{[}}}
\def \rsch	{\z@bigop{\hbox{]}}}
\def \dparallel	{\z@bigop{\parallel}\limits}
\def \zand	{\z@bigbin\land}
\def \zor	{\z@bigbin\lor}
\def \zcmp	{\z@bigbin\fcmp}
\def \zexi	{\z@bigop\exists}
\def \zall	{\z@bigop\forall}
\def \znot	{\z@bigop\neg}
\def \zbar	{\z@bigbin\cbar}
\def \zfor	{/}
\def \zhide	{\z@bigbin\backslash}
\def \zimp	{\z@bigrel\imp}
\def \zeq	{\z@bigrel\iff}
\def \zovr	{\z@bigrel\oplus}
\def \zpipe	{\z@bigbin{\mathord>\!\!\mathord>}}
\def \pre	{\keyword{pre}}
\def \pred	{\keyword{pred}}
\def \post	{\keyword{post}}
\def \zproject	{\z@bigbin\sres}
\def\rename{\@ifnextchar*{\z@rename}{\z@@rename}}
\def\z@rename*[#1/#2]{\left[#1 \over #2\right]}
\def\z@@rename[#1/#2]{\left[#1 \zfor #2\right]}
%	aliases
\let \project	\zproject
\let \import	\sres
\let \semi	\zcmp
\let \hide	\zhide
%
%	BAGS
%
\let\buni\uplus
\def \emptybag  {\lbag\:\rbag}
\def \lbag	{[\![}
\def \rbag	{]\!]}
\def \bag	{\keyword{bag}}
\def \items	{\word{items}}
\let \inbag	\inseq
\def \bagcount	{\word{count}}
%
%	DEFINITIONS & DECLARATIONS
%
\def \ddef	{\z@rel{\;::=\;}}
\def \bbar	{\z@bigrel\mid}
\let \cbar	\mid
\def \lang	{\langle\!\langle}
\def \rang	{\rangle\!\rangle}
\def \sdef	{\z@rel{\widehat=}}
\def \defs	{\z@smallrel{==}}
\def \varsdef	{\z@rel\triangleq}
%	aliases
\let \sdefs	\sdef
\mathcode`\|=\mid
\let \ldata	\lang
\let \rdata	\rang
%
%	MISCELLANEOUS
%
\def \lblot     {\langle\!|}
\def \rblot     {|\!\rangle}
\def \IMP	{\boldword{Import}}
\let \env	\Rrightarrow
\def \zlet      {\boldword{let}}
\def \zin       {\boldword{in}}
\def \zwhere	{\boldword{where}}
%
%	QZED SUPPORT
%
\def\HOLE{\z@op{\hbox{$\lll\star\star\star\ggg$}}}
\def\landd{} % to support qzed editor
\def\semid{} % to support qzed editor
\def\qzed{\ifz@inclass\else\zed\fi}
\def\endqzed{\ifz@inclass\else\endzed\fi}
%
%	CLASSES
%
\def\qua{\mbox{::}}
\def\redef{\mbox{\bf ~redef}}
\def\Init{I\!{\scriptstyle NIT}}
\def\Exit{E\!{\scriptstyle XIT}}
\def\Internal{I\!{\scriptstyle NTERNAL}}
\def\Aux{A\!{\scriptstyle UX}}
\def\intern{\mbox{\sf i}}
%
%		------ OTHER SPECIAL NOTATION ------
%
%	PROOFS
%
\def\thrm{\z@rel\vdash}
\def\qed{\zsmall\Box}
\let\Qed\Box
\let\QED\square
\def\BLACKQED{\zsmall\blacksquare}
\let\ETH\qed
\def\TH{\boldword{Theorem}}
\def\LE{\boldword{Lemma}}
\def\PR{\boldword{Proof}}
\def\refines{\z@rel\sqsupseteq}
\def\defines{\z@rel\sqsubseteq}
\def\weakrefine{\z@rel{\raise0.2ex\rlap{\hbox{$\sqsupset$}}\lower1ex\hbox{$\sim$}}}
\def\weakdefine{\z@rel{\raise0.2ex\rlap{\hbox{$\sqsubset$}}\lower1ex\hbox{$\sim$}}}
%	aliases
\let\shows\thrm
%
%	OBJECT THEORY
%
\def\childof{\z@rel\xsucc}
\def\parentof{\z@rel\xprec}
\let\weaksubclass\succsim
\let\weaksupclass\precsim
\def\hasa{\z@rel{\mathord\xsucc\!\!\!\mathord\xsucc}}
\def\instancein{\z@rel{\mathord\xprec\!\!\!\mathord\xprec}}
\def\subtype{\z@rel\sqsubset}
\def\subtypeeq{\z@rel\sqsubseteq}
\def\suptype{\z@rel\sqsupset}
\def\suptypeeq{\z@rel\sqsupseteq}
%	aliases
\let\inherits\childof
\let\subclass\childof
\let\isa\childof
\let\supclass\parentof
\let\instantiates\hasa
\let\islikea\weaksubclass
%
%	TEMPORAL LOGIC
%
\def\atnext{\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\zSmall\bigcirc$}\kern0.01em\zSmall\bigcirc}
\def\atlast{\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\kern0.01em\mathord-$}\zSmall\bigcirc}
\def\always{\lower0.37ex\hbox{$\zbig\Box$}}
\def\uptilnow{\rlap{$\kern0.02em\mathord-$}\lower0.37ex\hbox{$\zbig\Box$}}
\def\eventually{\lower0.37ex\hbox{$\zbig\Diamond$}}
\def\previously{\rlap{$\kern0.04em\mathord-$}\lower0.37ex\hbox{$\zbig\Diamond$}}
%	aliases
\let\henceforth\always
%
%	ORDERS
%
\def \mono	{\keyword{monotonic}}
\def \porder	{\keyword{partial\_order}}
\def \torder	{\keyword{total\_order}}
%
%	WORD STYLES
%
\def\String#1{\hbox{`{\tt #1}'}}
\def\STRING#1{\hbox{``{\tt #1}''}}
\def\infix#1{\z@rel{{\underline{#1}}}}
\def\word#1{\z@op{#1}}
\def\keyword#1{\z@op{\rm #1}}
\def\boldword#1{\z@op{\bf #1}}
\def\underword#1{\z@op{{\underline{#1}}}}
\def\underkeyword#1{\z@op{{\underline{\rm #1}}}}
\def\underboldword#1{\z@op{{\underline{\bf #1}}}}
\newbox\z@combox\newdimen\z@wdcalc
\def\comment{\@ifnextchar*{\z@leftcomment}{\z@comment}}
\def\z@comment#1{$\z@stopfield\z@addfield\z@startfield$\global\setbox\z@combox\hbox{\quad[{\sf #1}]}\z@wdcalc=\wd\z@combox\advance\z@wdcalc by \wd\z@curline\advance\z@wdcalc by \z@curindent\advance\z@wdcalc by \zedleftsep\advance\z@wdcalc by \zedlinethickness\advance\z@wdcalc by 2\zedindent\ifdim\z@wdcalc>\displaywidth\\\fi&\box\z@combox\ignorespaces}
\def\z@leftcomment*#1{\hbox{[{\sf #1}]}}
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%	SECTION 3	Z ENVIRONMENTS
%
%		------ MARGIN STACK ------
%
% define a stack of dimensions (50 elements)
%	can probably be made smaller when qzed filters its TeX output better
\newcount\z@stackmin
\newcount\z@stackmax
\newcount\z@stacktop
\newdimen\@gtempa \z@stackmin=\allocationnumber
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@getempa \z@stackmax=\allocationnumber
\dimen\z@stackmin=0pt

% define a box to contain the current line
%  & a variable to contain it's indentation
\newbox\z@curline
\newdimen\z@curindent
\dimen\z@curindent=0pt
% Space between operands of a function application
\def\z@space{{}\;{}}

% define a box to contain the current field
\newbox\z@curfield

% define a mini-tabbing environment for use inside 'zed'
\def\z@startline{\setbox\z@curline\hbox{}%
                 \global\z@curindent\dimen\z@stacktop
                 \z@startfield\ignorespaces}
\def\z@stopline{\z@stopfield
                \z@addfield
                \hbox{\hskip\z@curindent \box\z@curline}}

\def\z@startfield{\global\setbox\z@curfield\hbox\bgroup}
\def\z@stopfield{\egroup}
\def\z@addfield{\global\setbox\z@curline\hbox{\unhbox
                 \z@curline\unhbox\z@curfield}}

\def\z@pushmargin{\hbox{\kern0pt}$%
                  \z@stopfield
                  \z@addfield
                  \ifnum \z@stacktop < \z@stackmax
                    \global\advance\z@stacktop \@ne
                  \else
                    \@latexerr{Z margin stack overflow (too many \string\M's)}
		    \@ehd
                  \fi
                  \global\dimen\z@stacktop\z@curindent
                  \global\advance\dimen\z@stacktop \wd\z@curline
                  \z@startfield\ignorespaces
                  $\relax}
\def\z@popmargin{\ifnum \z@stacktop > \z@stackmin
                    \global\advance\z@stacktop \m@ne \ignorespaces
                  \else
                    \@latexerr{Z Margin stack underflow (too many \string\O's)}
		    \@ehd
                  \fi}
\def\M{\z@pushmargin} \def\O{\z@popmargin} \def\S{\z@space}
\z@stacktop\z@stackmin
%
%		------ UTILITY MACROS FOR Z ENVIRONMENTS ------
%
% Here are environments for the various sorts of displays which occur in
% Z documents. All displays are set flush left, indented by \zedindent,
% by default \leftmargini.  Schemas, etc, are made just wide enough to
% give equal margins left and right.
%
% Some environments (schema, etc.) must only be split at `\zbreak',
% and others (e.g. argue) may be split arbitrarily. All generate
% alignment displays, and penalties are used to control page breaks.
%
%	FORMAT and CONTROL macros
%
\newdimen\zedindent		\zedindent=\leftmargini
\newdimen\zedleftsep		\zedleftsep=1em
\newdimen\zedtab		\zedtab=2em
\newdimen\zedbar		\zedbar=8em
\newdimen\zedlinethickness	\zedlinethickness=0.4pt
\newdimen\zedcornerheight	\zedcornerheight=0pt
\newcount\z@cols
%
\newif\ifz@firstline		\z@firstlinefalse
\newif\ifz@inclass		\z@inclassfalse
\newif\ifz@inenv		\z@inenvfalse
\newif\ifz@leftmargin		\z@leftmargintrue
\newif\ifz@incols		\z@incolsfalse
\newif\ifleftnames		\leftnamesfalse
\def\leftschemas{\leftnamestrue}
\newif\ifz@inbox		\z@inboxfalse
%
\newskip\zedbaselineskip	\zedbaselineskip\baselineskip
\newbox\zstrutbox		\setbox\zstrutbox=\copy\strutbox
\def\zstrut{\relax\ifmmode\copy\zstrutbox\else\unhcopy\zstrutbox\fi}
\def\zedbaselinestretch{1}
%
% penalties
%
\newcount\interzedlinepenalty	\interzedlinepenalty=10000	%never break
\newcount\preboxpenalty		\preboxpenalty=0		%break easily
\newcount\forcepagepenalty	\forcepagepenalty=-10000	%always break
% also use			\interdisplaylinepenalty=100	%break sometimes
%
% macros for changing the size of schema text
%
\def\zedsize#1{\def\z@size{#1}}
\def\z@size{}
\newskip\z@adskip\newskip\z@bdskip\newskip\z@adsskip\newskip\z@bdsskip
\def\z@changesize{%
\z@adskip\abovedisplayskip\z@bdskip\belowdisplayskip% save skips
\z@adsskip\abovedisplayshortskip\z@bdsskip\belowdisplayshortskip
\z@size % change size
\abovedisplayskip\z@adskip\belowdisplayskip\z@bdskip% restore skips
\abovedisplayshortskip\z@adsskip\belowdisplayshortskip\z@bdsskip}
%
\def\zBIG#1{\hbox{\ifx\z@ptsize \vpt \viiipt\@viiipt
	\else \ifx\z@ptsize \vipt \ixpt\@ixpt
	\else \ifx\z@ptsize \viipt \xpt\@xpt
	\else \ifx\z@ptsize \viiipt \xipt\@xipt
	\else \ifx\z@ptsize \ixpt \xiipt\@xiipt
	\else \ifx\z@ptsize \xpt \xivpt\@xivpt
	\else \ifx\z@ptsize \xipt \xviipt\@xviipt
	\else \ifx\z@ptsize \xiipt \xxpt\@xxpt
	\else \ifx\z@ptsize \xivpt \xxvpt\@xxvpt
	\else \ifx\z@ptsize \xviipt \xxvpt\@xxvpt
	\else \ifx\z@ptsize \xxpt \xxvpt\@xxvpt
	\else \@warning{Can't increase this font size}
	\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi $\mathord{#1}$}}
\def\zBig#1{\hbox{\ifx\z@ptsize \vpt \viipt\@viipt
	\else \ifx\z@ptsize \vipt \viiipt\@viiipt
	\else \ifx\z@ptsize \viipt \ixpt\@ixpt
	\else \ifx\z@ptsize \viiipt \xpt\@xpt
	\else \ifx\z@ptsize \ixpt \xipt\@xipt
	\else \ifx\z@ptsize \xpt \xiipt\@xiipt
	\else \ifx\z@ptsize \xipt \xivpt\@xivpt
	\else \ifx\z@ptsize \xiipt \xviipt\@xviipt
	\else \ifx\z@ptsize \xivpt \xxpt\@xxpt
	\else \ifx\z@ptsize \xviipt \xxvpt\@xxvpt
	\else \ifx\z@ptsize \xxpt \xxvpt\@xxvpt
	\else \@warning{Can't increase this font size}
	\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi $\mathord{#1}$}}
\def\zbig#1{\hbox{\ifx\z@ptsize \vpt \vipt\@vipt
	\else \ifx\z@ptsize \vipt \viipt\@viipt
	\else \ifx\z@ptsize \viipt \viiipt\@viiipt
	\else \ifx\z@ptsize \viiipt \ixpt\@ixpt
	\else \ifx\z@ptsize \ixpt \xpt\@xpt
	\else \ifx\z@ptsize \xpt \xipt\@xipt
	\else \ifx\z@ptsize \xipt \xiipt\@xiipt
	\else \ifx\z@ptsize \xiipt \xivpt\@xivpt
	\else \ifx\z@ptsize \xivpt \xviipt\@xviipt
	\else \ifx\z@ptsize \xviipt \xxpt\@xxpt
	\else \ifx\z@ptsize \xxpt \xxvpt\@xxvpt
	\else \@warning{Can't increase this font size}
	\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi $\mathord{#1}$}}
\def\zsmall#1{\hbox{\ifx\z@ptsize \vipt \vpt\@vpt
	\else \ifx\z@ptsize \viipt \vipt\@vipt
	\else \ifx\z@ptsize \viiipt \viipt\@viipt
	\else \ifx\z@ptsize \ixpt \viiipt\@viiipt
	\else \ifx\z@ptsize \xpt \ixpt\@ixpt
	\else \ifx\z@ptsize \xipt \xpt\@xpt
	\else \ifx\z@ptsize \xiipt \xipt\@xipt
	\else \ifx\z@ptsize \xivpt \xiipt\@xiipt
	\else \ifx\z@ptsize \xviipt \xivpt\@xivpt
	\else \ifx\z@ptsize \xxpt \xviipt\@xviipt
	\else \ifx\z@ptsize \xxvpt \xxpt\@xxpt
	\else \@warning{Can't decrease this font size}
	\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi $\mathord{#1}$}}
\def\zSmall#1{\hbox{\ifx\z@ptsize \vipt \vpt\@vpt
	\else \ifx\z@ptsize \viipt \vpt\@vpt
	\else \ifx\z@ptsize \viiipt \vipt\@vipt
	\else \ifx\z@ptsize \ixpt \viipt\@viipt
	\else \ifx\z@ptsize \xpt \viiipt\@viiipt
	\else \ifx\z@ptsize \xipt \ixpt\@ixpt
	\else \ifx\z@ptsize \xiipt \xpt\@xpt
	\else \ifx\z@ptsize \xivpt \xipt\@xipt
	\else \ifx\z@ptsize \xviipt \xiipt\@xiipt
	\else \ifx\z@ptsize \xxpt \xivpt\@xivpt
	\else \ifx\z@ptsize \xxvpt \xviipt\@xviipt
	\else \@warning{Can't decrease this font size}
	\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi $\mathord{#1}$}}
%
\def\z@zeroskips{\abovedisplayskip\z@\belowdisplayskip\z@
	\abovedisplayshortskip\z@\belowdisplayshortskip\z@}
%
%	Make zedbaselinestretch have an automatic effect
%		adapted from lfonts.tex
%
\def\@setsize#1#2#3#4{\@nomath#1\let\@currsize#1\baselineskip
	#2\baselineskip\baselinestretch\baselineskip
	\setbox\strutbox\hbox{\vrule height.7\baselineskip
	depth.3\baselineskip width\z@}\normalbaselineskip
	\baselineskip #3#4\zedbaselineskip
	#2\zedbaselineskip\zedbaselinestretch\zedbaselineskip
	\setbox\zstrutbox\hbox{\vrule height.7\zedbaselineskip
	depth.3\zedbaselineskip width\z@}\let\z@ptsize#3}
%
%		------ MACROS FOR MARGINS ------
%
% \z@narrow, \z@wide - make the margins narrower, wider
%
\def\z@narrow{\advance\linewidth by -\zedindent}
\def\z@wide{\advance\linewidth by \zedindent}
%
%		------ MACROS FOR DRAWING BOXES ------
%
% \z@hrulefill - line with correct thickness
%
\def\z@hrulefill{\leaders\hrule height\zedlinethickness\hfill}
%
% \z@topline draws the top horizontal line of boxed environments
% \z@dbltopline draws a double ruled top line
% \z@botline draws the bottom horizontal line of boxed environments
% \zedline[comment] draws a long horizontal line ending in comment
% \where draws a short horizontal line
%
\def\z@topline#1{\omit\@ifnextchar[{\z@@topline{#1}}{\z@@topline{#1}[]}}
\def\z@@topline#1[#2]{\hbox to\linewidth{\zstrut\ifleftnames\else
	\vrule height\zedlinethickness width\zedlinethickness
	\hbox to\zedleftsep{\z@hrulefill}\fi#1\z@hrulefill
	\smash{\vrule height\zedlinethickness width\zedlinethickness
	depth\zedcornerheight}\hbox{\sf #2}}\cr}
\def\z@dbltopline#1{\omit\@ifnextchar[{\z@@dbltopline{#1}}{\z@@dbltopline{#1}[]}}
\def\z@@dbltopline#1[#2]{\z@@topline{#1}[#2]%
\noalign{\kern-\baselineskip
	\kern-\zedlinethickness
	\kern-\doublerulesep \nobreak}%
\omit\z@@topline{\hphantom{#1}}[\hphantom{#2}]%
\noalign{\kern\doublerulesep
	\kern\zedlinethickness \nobreak}}
\def\z@botline{\also\omit\hbox to\linewidth{\z@hrulefill
\smash{\vrule height\zedcornerheight width\zedlinethickness
        depth 0pt}}\cr}
\def\z@@botline[#1]{\hbox to\linewidth{\vrule\z@hrulefill\hbox{\sf\smash{#1}}}\also}
\def\zedline{\also\omit\@ifnextchar[{\z@@botline}{\z@@botline[]}}
\def\where{\also \omit \hbox to\zedbar{\z@hrulefill}\cr\also}
\let \ST	\where
%
% \z@left is placed at the left of each z line:
%	in non-box environments it will do nothing.
%	in boxed environments it will do a vertical line with the same
%		height as the maximum height of the line.
%
\def\z@left{\ifz@inbox\vrule width\zedlinethickness\hskip\zedleftsep\fi}
%
%		------ MACROS FOR SETTING UP Z ENVIRONMENTS ------
%
\def\z@env{\global\z@firstlinetrue\z@changesize
	$$\z@inenvtrue\baselineskip\zedbaselineskip
	\parskip=0pt\lineskip=0pt\z@narrow
	\advance\displayindent by \zedindent
        \def\\{\crcr}% Must have \def and not \let for nested alignments.
        \everycr={\noalign{\ifz@firstline \global\z@firstlinefalse
                \else \penalty\interzedlinepenalty \fi}}
        \tabskip=0pt}
\def\endz@env{$$\global\@ignoretrue}
%
% z lines are formated in two (overlaping) columns;
%	the first flush left having the same width as the environment,
%	and, the second flush right ending at the right end of the environment.
%
\def\z@format{\halign to\linewidth\bgroup%
        \zstrut\z@left\z@startline\ignorespaces$\@lign##$\z@stopline\hfil%
        \tabskip=0pt plus1fil%
        &\hbox to 0pt{\hss\@lign##}\tabskip=0pt\cr}
%
\def\z@boxenv{\z@narrow\let\also=\als@ \let\Also=\Als@ \let\ALSO=\ALS@
	\z@inboxtrue \predisplaypenalty=\preboxpenalty \z@env\z@format}
%
\def\z@outnonbox{\z@outclasscheck\z@leavevmode\z@env}
\def\z@inoutbox{\z@leavevmode\z@makeouter\z@inclassfalse\z@boxenv}
%
%	SPACING COMMANDS
%
% no vertical glue between abutted lines
%
\def\@but{\noalign{\nointerlineskip}}
%
% no \par extra vertical spacing after Z environments
%
%\def\z@nopar{\ifz@inclass\else\vskip-\parskip\fi}
%\def\z@nopar{\global\parskip0pt\global\everypar{\parskip30mm\everypar{}}}
\def\z@nopar{\global\@endpetrue}
%
% \z@leavevmode -- Enter horizontal mode, taking account of possible
% interaction with lists and section heads:
%
%	1	After a \item, use \indent to get the label (this
%		fails to run in even short labels).
%	2	After a run-in heading, use \indent.
%	3	After an ordinary heading, throw away the \everypar
%		tokens, reset \@nobreak, and use \noindent with \parskip
%		zero.
%	4	Otherwise, use \noindent with \parskip zero
%
% use when entering displayed environments to get correct spacing
%
\def\z@leavevmode{\ifvmode\if@inlabel\indent\else\if@noskipsec\indent\else
	\if@nobreak\global\@nobreakfalse\everypar={}\fi
	{\parskip=0pt\noindent}\fi\fi\fi}
%
% extra vertical space in non-box environments
%
\def\also{\crcr\noalign{\vskip\jot}}
\def\Also{\crcr\noalign{\vskip2\jot}}
\def\ALSO{\Also\Also}
%
% extra vertical space in boxed environments
%
\def\als@{\crcr\@but\omit\vrule height\jot width\zedlinethickness \cr \@but}
\def\Als@{\crcr\@but\omit\vrule height2\jot width\zedlinethickness \cr \@but}
\def\ALS@{\crcr\@but\omit\vrule height4\jot width\zedlinethickness \cr \@but}
%
%	ENVIRONMENT-BREAKING COMMANDS
%
\def\znewpage{\also\noalign{\penalty\forcepagepenalty}\also}
\def\zbreak{\also\noalign{\penalty\interdisplaylinepenalty\vskip-\jot}\also}
\def\Zbreak{\also\noalign{\penalty\interdisplaylinepenalty}\also}
\def\ZBREAK{\Also\noalign{\penalty\interdisplaylinepenalty}\Also}
%
\def\t#1{\hskip #1\zedtab}
\def\c#1#2{\hbox to #1\zedtab{$#2$\hfil}}
\def\flushr#1{\crcr&#1\quad\cr}
%
%		------ UTILITY MACROS FOR OBJECT-Z ------
%
\def\z@inclasscheck{\ifz@inclass\else
	\@latexerr{This Z environment is only allowed within a class}
{Perhaps you forgot to include a \string\begin\string{class\string}
somewhere^^Jor you are trying to print a file that needs updating.^^J\@ehc} \fi}
\def\z@outclasscheck{\ifz@inclass
	\@latexerr{This Z environment is not allowed inside a class}
{This environment doesn't really make sense within a class.^^J%
If you really want it then I'll try my best to fit in in.^^J\@ehc}\else
\ifz@inenv \@latexerr{New Z environment declared before previous
one is completed}
{I suspect that you've forgotten to finish the last environment.^^J%
You are trying to nest environments and this can only be done inside classes^^J%
besides, the environment you have started isn't valid within classes any way.^^JI suggest that you type \space X <return> \space to quit and then correct your document.}
\fi\fi}
%
\def\z@makeouter{\ifz@inenv\ifz@inclass\z@inenvfalse
	\hskip-\zedleftsep \advance\linewidth by -\zedlinethickness
	\zedindent=\zedleftsep \zedleftsep=0.8\zedleftsep
	\zedbar=0.8\zedbar \zedtab=0.8\zedtab
	\parbox[b]{\linewidth}\bgroup\z@zeroskips
	\else\@latexerr{Incorrect place for Z environment; nesting is
allowed only inside classes}
{You've either forgotten to finish the last environment,^^J%
you've forgotten to include a \string\begin\string{class\string} somewhere^^J%
or you are trying to print a file that needs updating.^^J%
(Then again, you might just be trying to do something^^J%
that the author of these macros didn't intend you to do)^^J\@ehc}
	\fi\else\bgroup\fi}
%
\def \z@makeinner{\egroup%
\global\z@curindent\z@}
%
\def \classbreak{\also\egroup$$\vskip -\ht\zstrutbox
	\vskip -\abovedisplayskip\vskip -\belowdisplayskip\z@wide\z@boxenv\also}
%
%		------ NON-BOX ENVIRONMENTS ------
%

%
%	ZED			for non-box multiline formulas
%
\def\zed{\z@outnonbox\z@inboxfalse\z@format}
\def\endzed{\crcr\egroup\endz@env}
\let\[=\zed
\def\]{\crcr\egroup$$\ignorespaces}
%
%	ARGUE			for algebraic arguments
%
%	used for algebraic proofs expressed as extended equations.
%	like zed but with extra spacing between lines
%	Generates an alignment display, which may be split across pages.
%
\def\argue{\z@outnonbox\interzedlinepenalty=\interdisplaylinepenalty
	\openup 1\jot \z@format
	\noalign{\vskip-\jot}}% equal vspace above and below argue display
\let\endargue=\endzed
%
%	INFRULE			for inference rules
%
%	used for inference rules. The horizontal line is generated by \derive:
%	an optional argument contains the side-conditions of the rule.
%
\def\infrule{\z@outnonbox\halign\bgroup
	\zstrut\quad$\@lign##$\quad\hfil&\quad\@lign##\hfil\cr}
\let\endinfrule=\endzed
\def\derive{\crcr\also\@but\omit\z@hrulefill%
	\@ifnextchar[{\z@sidecondition}{\cr\also\@but}}
\def\Derive{\crcr\also\@but\omit\z@hrulefill\cr\@but
        \noalign{\kern-\dp\zstrutbox
	\kern\doublerulesep \nobreak}%
\omit\derive}
\def\z@sidecondition[#1]{&$\smash{\lower 0.2ex\hbox{$[\;#1\;]$}}$\cr\also\@but}
%
%	SYNTAX			for syntax rules
%
% `syntax' environment: used for syntax rules - even (once!) for VDM.
\def\syntax{\z@outnonbox\halign\bgroup
	\zstrut$\@lign##$\hfil &\hfil$\@lign{}##{}$\hfil
	&$\@lign##$\hfil &\qquad\@lign-- ##\hfil\cr}
\let\endsyntax=\endzed

%
%		------ BOXED ENVIRONMENTS ------
%
%
%	SCHEMA			schema definitions
%
\def\schema#1{\z@inoutbox\z@topline{$\,#1\,$}}
\def\endschema{\z@botline \endzed \z@makeinner \z@nopar}
%
%	SCHEMA*			schema with no name
%
\@namedef{schema*}{\leftnamesfalse\z@inoutbox\z@topline{}}
\expandafter\let\csname endschema*\endcsname=\endschema
%
%	GENSCHEMA		generic schema definitions
%
\def\genschema#1#2{\z@inoutbox\z@topline{$\,#1\:[#2]\,$}}
\let\endgenschema=\endschema
%
%	AXDEF			'liberal' axiomatic definitions
%
\def\axdef{\z@inoutbox}
\def\endaxdef{\endzed\z@makeinner}
%
%	UNIQDEF			'unique' axiomatic definitions
%
\def\uniqdef{\leftnamesfalse\z@inoutbox\z@dbltopline{}}
\let\enduniqdef=\endschema
%
%	GENDEF			'generic' axiomatic definitions
%
\def\gendef#1{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,[#1]\,$}}
\let\endgendef=\endschema
%
%	CLASS
%
\def\class#1{\z@leavevmode\z@makeouter\z@inclasstrue
		\z@boxenv\z@topline{$\,#1\,$}}
\let\endclass\endschema
%
%	OP
%
\def\op{\z@inclasscheck\schema}
\let\endop\endschema
%
%	STATE
%
\def\state{\z@inclasscheck\vbox\bgroup\vskip-\ht\zstrutbox\vbox\bgroup\hbox\bgroup\@nameuse{schema*}}
\def\endstate{\endschema\egroup\egroup\egroup}
%
%	INIT
%
\def\init{\z@inclasscheck\schema{\Init}}
\let\endinit\endschema
%
%		------ OTHER ENVIRONMENTS ------
%
%	SIDEBYSIDE
%
% This should support an arbitary number of columns
%	\zedindent's proportion of \linewidth gives a practical limit
%
\def\sidebyside{\@ifnextchar[{\z@columns}{\z@columns[2]}}
\def\z@columns[#1]{\z@leavevmode\z@cols#1 \z@makeouter\z@narrow%
	$$\lineskip=0pt\z@incolstrue
	\predisplaysize\maxdimen
	\ifz@leftmargin\hskip-\zedindent\z@leftmarginfalse\fi
	\setbox0=\hbox to \linewidth\bgroup\z@zeroskips%
	\divide\zedbar by \z@cols \divide\zedleftsep by \z@cols
	\divide\zedtab by \z@cols \divide\linewidth by \z@cols
	\parbox[t]{\linewidth}\bgroup\z@wide}
%
\def\nextside{\egroup\hss\parbox[t]{\linewidth}\bgroup\z@wide}
%
\newdimen\z@temp
\def\endsidebyside{\egroup\egroup
	\z@temp\ht0 \advance\z@temp by \dp0\advance\z@temp by-\dp\zstrutbox
	\hbox{\raise\z@temp\box0}\endz@env\z@makeinner\z@nopar}
%
%	ZPAR
%
\def\zpar{\z@leavevmode
	\ifz@inenv\z@inclasstrue\fi% fudge to let zpar in all boxes
	\z@makeouter\z@changesize
	\advance\linewidth by -\z@curindent
	\advance\linewidth by -\wd\z@curline
	\hskip-\wd\z@curline\advance\linewidth by -\zedindent$$
	\ifz@leftmargin\hskip-\zedindent\fi% adjustment for first column
	\advance\displayindent by \zedindent
	\advance\displaywidth by -\zedindent
	\advance\displayindent by \z@curindent
	\advance\displayindent by \wd\z@curline
	\advance\displaywidth by -\z@curindent
	\advance\displaywidth by -\wd\z@curline
	\global\setbox\z@curline\hbox{}
	\z@narrow\parbox[b]{\linewidth}\bgroup\hfil\break}
\def\endzpar{\egroup$$\z@makeinner\z@nopar}
%
%	CLASSCOM
%
\def \classcom{\zpar\sf}
\let \endclasscom=\endzpar
%
%	PROOF
%
\def\proof{\zpar$\PR$\zpar}
\def\endproof{\endzpar\endzpar}
%
% Additional auxiliary macros
%
\def\zseq#1{\lseq #1 \rseq}
\def\zset#1{\{ #1 \}}
\def\zimg#1{\limg #1 \rimg}
\def\zsch#1{\lsch #1 \rsch}
\def\zimgset#1{\zimg\zset{#1}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%
%%%%%		FUTURE UPDATES:
%%%%%
%%%%% investigate the setting of \par to minimise space after schemas & zpars
%%%%% make display skips bigger for large fonts
%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%