[comp.text.tex] Wanted: LaTeX macros for Z and Object-Z

king@batserver.cs.uq.oz.au (Paul King) (12/14/90)

In response to <70136@unix.cis.pitt.edu> jordan@unix.cis.pitt.edu (Kenneth D Jordan) here is part 1 of the Object-Z macros:

Here are the macros you asked for.  I'll send what you need in 2 parts.
This is part 1 - it contains the actual 'oz.sty' macro package
(The macros are set up to use the old AMSTeX fonts but can easily be adapted
for the new fonts - see the note in oz.sty about this).

If you want to know more about Object-Z please contact me.

Have fun, Paul King.

----------------------------cut here for oz.sty-------------------------
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% 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
%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
----------------------------end of oz.sty----------------------------
--
Paul King							       _--_|\
Dept. of Computer Science, Univ. of Queensland			      /      X
Queensland, Australia, 4072					      \_.--._/
king@batserver.cs.uq.oz.au (ACSNET)				            v

king@batserver.cs.uq.oz.au (Paul King) (12/14/90)

In response to <70136@unix.cis.pitt.edu> jordan@unix.cis.pitt.edu
(Kenneth D Jordan) here is the documentation for the Object-Z (and Z) macros:

Here is part 2 - oz.tex, threecolumn.sty
you will need both of these to produce the documentation - they
are not required to use the oz.sty macro package.
I did not write 'threecolumn.sty'.

Let me know if you have any problems
and please feel free to suggest (and/or implement)
any enhancements to the package,
					Paul King

P.S.  The very latest changes (see the history in oz.sty)
      may not be documented (yet). 

-------------------------cut here for oz.tex-----------------------
\documentstyle[11pt,oz,threecolumn]{article}
% you may need to change some of the dimensions below to position
% the document correctly on the page (depending on your local printer setup).
% alw - document DOESN'T PRINT in one go on the alw, print a few pages at a time
\oddsidemargin -2mm
\evensidemargin -2mm
\topmargin 0mm
\textwidth 188mm
\textheight 256mm
\headheight 0 pt
\headsep 0 pt
\footheight 16 pt
\footskip 24 pt
\parskip 4 pt
\parindent 0 pt
%
% just ignore any over- or under-full hboxes
% this document uses most of the (physical) page and isn't spread
% out either.  This may make it slightly harder to read first time
% through, but makes it more suitable for later reference.
%
% before we start, let's make a few definitions
%
\makeatletter
\def\example{\begin{sidebyside}}
\def\verbpart{\nextside\small\vspace*{-1ex}\begin{quote}\begin{verbatim}}
\def\endexample{\end{quote}\vspace*{-2ex}\end{sidebyside}\vspace*{-3ex}\ignorespaces}
\def\symbol#1{#1 & \tt\string#1}
\def\symbols{\@ifnextchar[{\@symbols}{\@symbols[0]}}
\def\@symbols[#1]{\interzedlinepenalty=\interdisplaylinepenalty\z@env
        \openup #1\jot
	\halign\bgroup\zstrut\hbox to 3.8em{$##$\hss}\tabskip=0pt&##\hss\cr
        \noalign{\vskip-#1\jot}}% equal vspace above and below argue display
\let\endsymbols=\endzed
\makeatother
%
\begin{document}
\begin{center}
{\Large\bf Printing Z and Object-Z \LaTeX\ documents}\\[2.5ex]
{\em Paul King}\\[1ex]
Department of Computer Science\\
University of Queensland\\
Australia, 4072\\
king@batserver.cs.uq.oz.au\\[1ex]
May 29, 1990
\end{center}

\section{Introduction}
This note describes a package of \LaTeX\ macros for printing
Z and Object-Z specifications.  The macros and this note are
based originally on Mike Spivey's \verb'zed.sty' macros and documentation.
The package does several related things for you:
\begin{itemize}
\item   It loads extra fonts and defines mnemonics
	for the Z symbols they contain.
\item   It defines macros for some Z symbols (e.g. $\pinj$) which
        don't appear in any of our fonts.
\item   It fixes the way \TeX\ sets letters in mathematical formulas so
        that multi-character identifiers look better.
\item   It provides various brands of `boxed mathematics'
        which appear in Z and Object-Z specifications.
\end{itemize}

The package is kept in a file {\tt oz.sty}
in the directory \verb|/usr/local/lib/tex/localinputs|.
This directory should be mentioned in your \verb|TEXINPUTS| shell variable.
To use the macros you just begin your \LaTeX\ document with something like:
\begin{quote}
\begin{verbatim}
\documentstyle[11pt,oz]{article}
\end{verbatim}
\end{quote}
\vspace*{-1.5ex}

\section{Schema Boxes}

The example below shows a schema on the left and what you
need to say to get it on the right.

\begin{example}
\begin{schema}{BirthdayBook}
    known: \pset NAME \\
    birthday: NAME \pfun DATE
\ST
    known = \dom birthday
\end{schema}
\verbpart
\begin{schema}{BirthdayBook}
    known: \pset NAME \\
    birthday: NAME \pfun DATE
\ST
    known = \dom birthday
\end{schema}
\end{verbatim}
\end{example}

The command \verb|\ST| (read `Such That') is the same as the previously used
command \verb|\where| which has been kept as an alias for upward compatibility.
If you want a schema with no name, just a horizontal rule at the top,
use the \verb|schema*| environment instead.
You can set various parameters (see Section 7) to change the box style,
for example:

\begin{example}
\begin{leftschemas}
\zedcornerheight=3ex\zedlinethickness=0.9pt
\zedbar=10em\zedleftsep=1.5em
\begin{schema}{BirthdayBook}
    known: \pset NAME \\
    birthday: NAME \pfun DATE
\ST
    known = \dom birthday
\end{schema}
\end{leftschemas}
\nextside\small\vspace{-1ex}
\begin{quote}
In document preamble: \hfil\\
~~\verb|\leftschemas|\hfil\\
~~\verb|\zedcornerheight=3ex|\hfil\\
~~\verb|\zedlinethickness=0.9pt|\hfil\\
~~\verb|\zedbar=10em\zedleftsep=3em|\hfil\\
\end{example}

Schemas can also be defined using a horizontal notation, for example:
\begin{example}
\begin{zed}
BirthdayBook \sdef \lsch \ldots \rsch
\end{zed}
\verbpart
$BirthdayBook \sdef \lsch ... \rsch$
\end{verbatim}
\end{example}

A generic schema is produced as follows.

\begin{example}
\begin{genschema}{Pool}{RESOURCE}
owner : RESOURCE \pfun USER \\
free : \pset RESOURCE
\ST
(\dom owner) \uni free = RESOURCE \\
(\dom owner) \int free = \emptyset
\end{genschema}
\verbpart
\begin{genschema}{Pool}{RESOURCE}
owner : RESOURCE \pfun USER \\
free : \pset RESOURCE
\ST
(\dom owner) \uni free = RESOURCE \\
(\dom owner) \int free = \emptyset
\end{genschema}
\end{verbatim}
\end{example}

\section{Axiomatic definitions}

A `liberal' axiomatic definition is produced as follows.

\vspace{-1ex}\begin{example}
\vspace{\ht\zstrutbox}
\begin{axdef}
limit : \nat
\ST
limit \leq 65536
\end{axdef}
\verbpart
\begin{axdef}
limit : \nat
\ST
limit \leq 65536
\end{axdef}
\end{verbatim}
\end{example}

A `generic' axiomatic definition is produced as follows.

\begin{example}
\begin{gendef}{X,Y}
first : X \prod Y \tfun X
\ST
\all x : X; y : Y \dot first(x,y) = x
\end{gendef}
\verbpart
\begin{gendef}{X,Y}
first : X \prod Y \tfun X
\ST
\all x : X; y : Y \dot first(x,y) = x
\end{gendef}
\end{verbatim}
\end{example}

A `unique' axiomatic definition is produced as follows.

\begin{example}
\begin{uniqdef}
\pi : \real
\ST
\pi = 3.14159265\ldots
\end{uniqdef}
\verbpart
\begin{uniqdef}
\pi : \real
\ST
\pi = 3.14159265\ldots
\end{uniqdef}
\end{verbatim}
\end{example}

\section{Object-Z Class Boxes}

Object-Z allows class types to be defined using a box very
similar to the schema box previously described.
It allows the previously described boxed environments
(as well as nested sub-classes) to be placed within a class box.
%
In addition, special names can be used for some of the boxed-environments
when they appear within a class box.
The following example illustrates a class definition.

\begin{example}
\begin{class}{Shape}
\also
colour : Colour \\
\begin{axdef}
perim : \real
\ST
perim > 0
\end{axdef} \\
\begin{classcom}
This class has 2 constants
$colour$ and $perim$.
\end{classcom} \\
\begin{state}
x, y : \real
\end{state} \\
\begin{init}
x = y = 0
\end{init} \\
\begin{op}{Translate}
\Delta (x,y) \\
dx?, dy? : \real
\ST
x' = x + dx? \\
y' = y + dy?
\end{op}
\end{class}
\verbpart
\begin{class}{Shape}
\also
colour : Colour \\
\begin{axdef}
perim : \real
\ST
perim > 0
\end{axdef} \\
\begin{classcom}
This class has 2 constants
$colour$ and $perim$.
\end{classcom} \\
\begin{state}
x, y : \real
\end{state} \\
\begin{init}
x = y = 0
\end{init} \\
\begin{op}{Translate}
\Delta (x,y) \\
dx?, dy? : \real
\ST
x' = x + dx? \\
y' = y + dy?
\end{op}
\end{class}
\end{verbatim}
\end{example}

The \verb|classcom| environment hasn't been seen before.
It creates a paragraph of text with the same margins as used
for schemas and other Z environments.  It uses a special font
intended for use when placing comments inside classes.
A similar environment, \verb|zpar|, uses the same margins
but with the normal roman font.

The \verb|\begin{init}| command is an abbreviation for
\verb|\begin{schema}{\Init}|.  Similarly \verb|\begin{state}|
is a more meaningful synonym for \verb|\begin{schema*}|.

You will be given \LaTeX\ warning messages if you try to
use a \verb|state| environment outside of a class box
or if you try to place an environment such as \verb|syntax|
inside a class.  You can ask for additional help in these
cases using the normal \LaTeX\ \verb|h| or \verb|H| help commands.
If you proceed with \LaTeX ing, the macros will attempt to
do the best they can to do what you probably intend, even though
you are violating the recommended nesting guidelines.

\section{Controlling the Spacing within Equations and Boxes}

Most of the special Z symbols are defined
in a way that allows \TeX\ to space them out correctly.
Sometimes, however, you'll need to give \TeX\ a helping hand if
you want it to get the spacing right.  For example, to get $map\,f$
you need to type \verb|map\,f|.  The \verb|\,| gives you a thin space:
if this is omitted, the input \verb|map f| gives
$map f$, because \TeX\ ignores spaces in math mode.

Sometimes it is useful to indent the left margin to emphasis
the logical structure of the predicate.
The command \verb|\t1| does this by making the corresponding
line in the output have one helping of indentation.
As things get more nested, you can say \verb|\t2|, \verb|\t3|, and so on.
But if you should ever get beyond \verb|t9|, you'll need to use braces
around the argument: \verb|\t{10}|, and you'd better look for some way
to simplify your specification!
These little tab marks might look different to normal tabs
but are never the less convenient. They're short,
and they don't get longer as the tabbing gets deeper, within reason,
so they can be tucked in neatly on the left, well away from the maths.
The size of `helping' you get with \verb|\t| is determined by
the \verb|\zedtab| parameter (see Section 7).

If you want a more powerful aligning mechanism than tabbing
then you can use the margin stack as shown in the example below.
The command \verb|\M| sets the future left margin to the current
horizontal position and pushes the old value onto a margin stack.
The command \verb|\O| resets the left margin to its previous value
(which is popped off the stack).

\begin{example}
\begin{schema}{Test}
x, y : \nat
\ST
x + 1/x = 0 \imp \M y + 1/y = 0 \\
y = x \O \\
\end{schema}
\verbpart
\begin{schema}{Test}
x, y : \nat
\ST
x + 1/x = 0 \imp \M y + 1/y = 0 \\
y = x \O \\
\end{schema}
\end{verbatim}
\end{example}

If a schema or other box contains more than one predicate below the
line, it often looks better to add a tiny vertical space between
them, as in this example:

\begin{example}
\begin{schema}{AddBirthday}
  \Delta BirthdayBook \\
  n?: NAME \\
  d?: DATE
\ST
  n? \nem known
\also
  birthday' = birthday \uni \{n? \map d?\}
\end{schema}
\verbpart
\begin{schema}{AddBirthday}
  \Delta BirthdayBook \\
  n?: NAME \\
  d?: DATE
\ST
  n? \nem known
\also
  birthday'=birthday \uni \{n? \map d?\}
\end{schema}
\end{verbatim}
\end{example}

This is done with the command \verb|\also|, which behaves syntactically
like \verb|\ST|.
The command \verb|\also| is provided {\em instead\/} of the
optional argument to \verb|\\|
which \LaTeX\ provides in other environments.
If larger vertical spacing is required, the commands
\verb|\Also| and \verb|\ALSO| may be used (giving 2 and 4 times
as much space as \verb|\also| respectively).

Normally, the contents of a schema box are kept on a single page.
For large schemas it may be necessary to split the box across pages.
You must specify which places are suitable for splitting using one of
\verb|\zbreak|, \verb|\Zbreak| or \verb|\ZBREAK|.  If no split is
performed at this point, a vertical space will be added as if the
user had typed \verb|\also|, \verb|\Also|, or \verb|\ALSO| respectively.
You can also use the \verb|\znewpage| command to force a page break within
a box.  (These breaking facilities will hopefully never be needed for schemas,
but may become necessary for class specifications.)

\section{Other Display Environments}

The \verb|zed| environment can be used to set multi-line formulas without
an enclosing box: it is useful for given-set declarations, theorems, and the
miscellaneous bits of mathematics that don't come in a box:

\vspace{-1ex}\begin{example}
\vspace{\ht\zstrutbox}
\begin{zed}
    \all n: \nat \dot \\
\t1         n+n \mem even.
\end{zed}
\verbpart
\begin{zed}
    \all n: \nat \dot \\
\t1         n+n \mem even.
\end{zed}
\end{verbatim}
\end{example}

The formula \verb|\begin{zed} ... \end{zed}| may be abbreviated to
\verb|\[ ... \]|; the \verb|zed| environment is a generalization of the
\verb|displaymath| environment of \LaTeX, so this redefinition of
commands is fairly benign. Notice that the maths is set flush left on the
same indentation as schemas and their friends.
Here too you can use \verb|\also| for a little extra space
between lines.

For algebraic-style proofs, there is the \verb|argue| environment.
This is like the \verb|zed| environment, but the separation between
lines is increased a little, and page breaks may occur between lines.
When the left-hand side is long this style wastes less space
than the \LaTeX\ \verb|eqnarray| style.
The intended use is for arguments like this:
\begin{argue}
    rev(append(cons(x,s),t)) \\
\t1     = rev(cons(x,append(s,t))) \\
\t1     = append(rev(append(s,t)),cons(x,nil)) \\
\t1     = append(append(rev(t),rev(s)),cons(x,nil))
                \quad \hbox{by hypothesis} \\
\t1     = append(rev(t),append(rev(s),cons(x,nil))) \\
\t1     = append(rev(t),rev(cons(x,s))).
\end{argue}
Here is the input:
\begin{quote}
\begin{verbatim}
\begin{argue}
    rev(append(cons(x,s),t)) \\
\t1     = rev(cons(x,append(s,t))) \\
\t1     = append(rev(append(s,t)),cons(x,nil)) \\
\t1     = append(append(rev(t),rev(s)),cons(x,nil))
                \quad \hbox{by hypothesis} \\
\t1     = append(rev(t),append(rev(s),cons(x,nil))) \\
\t1     = append(rev(t),rev(cons(x,s))).
\end{argue}
\end{verbatim}
\end{quote}

The example below shows an inference rule (the optional argument
to \verb|\derive| gives a side-condition of the rule):

\vspace{-1ex}\begin{example}
\vspace{\ht\zstrutbox}
\begin{infrule}
    \Gamma \shows P
\derive[x \nem freevars(\Gamma)]
    \Gamma \shows \all x \dot P
\end{infrule}
\verbpart
\begin{infrule}
    \Gamma \shows P
\derive[x \nem freevars(\Gamma)]
    \Gamma \shows \all x \dot P
\end{infrule}
\end{verbatim}
\end{example}

The \verb|syntax| environment is used for making displays like this:

\begin{syntax}
  EXPR & \ddef & IDENT      & identifier \\
       & \bbar & EXPR\;EXPR & application \\
       & \bbar & \lambda IDENT \dot EXPR & lambda-abstraction.
\end{syntax}
from input like this:
\begin{quote}
\begin{verbatim}
\begin{syntax}
  EXPR & \ddef & IDENT                   & identifier \\
       & \bbar & EXPR\;EXPR              & application \\
       & \bbar & \lambda IDENT \dot EXPR & lambda-abstraction.
\end{syntax}
\end{verbatim}
\end{quote}

This kind of thing is useful when you're describing a language,
and it can also be used for data-type definitions as shown below.
The optional final column was omitted below by leaving out the third \verb|&|.

{\small
\vspace{-1ex}\begin{example}
\vspace{0.5\ht\zstrutbox}
\begin{syntax}
TYPE & \ddef & givenT  \lang NAME \rang \\
     & \bbar & powerT  \lang TYPE \rang \\
     & \bbar & tupleT  \lang \seq TYPE \rang \\
     & \bbar & schemaT \lang IDENT \ffun TYPE \rang \\
     & \bbar & classT  \lang IDENT \ffun ClassAttr \rang \\
\end{syntax}
\verbpart
\begin{syntax}
TYPE & \ddef & givenT  \lang NAME \rang \\
& \bbar & powerT \lang TYPE \rang \\
& \bbar & tupleT \lang \seq TYPE \rang \\
& \bbar & schemaT \lang IDENT \ffun TYPE \rang \\
& \bbar & classT \lang IDENT \ffun ClassAttr \rang
\end{syntax}
\end{verbatim}
\end{example}}

This can be compared with the layout adopted by the UQ Z editor (version 1).

{\small
\vspace{-1ex}\begin{example}
\vspace{0.5\ht\zstrutbox}
\begin{zed}
TYPE \ddef \M givenT  \lang NAME \rang \\
     \bbar powerT  \lang TYPE \rang \\
     \bbar tupleT  \lang \seq TYPE \rang \\
     \bbar schemaT \lang IDENT \ffun TYPE \rang \\
  \bbar classT  \lang IDENT \ffun ClassAttr \rang \O
\end{zed}
\verbpart
\begin{zed}
TYPE \ddef \M givenT  \lang NAME \rang \\
\bbar powerT \lang TYPE \rang \\
\bbar tupleT \lang \seq TYPE \rang \\
\bbar schemaT \lang IDENT \ffun TYPE \rang \\
\bbar classT \lang IDENT \ffun ClassAttr \rang \O
\end{zed}
\end{verbatim}
\end{example}}

The {\tt sidebyside} environment allows a display as shown in the
first two columns below to be produced from the text of the third column.
Note the use of the \verb|\comment| command.

\begin{example}
\begin{sidebyside}
\begin{schema}{Schema}
\comment*{declarations}
\ST
a < b & [{\sf pred-1}]\\
aaaaa < bbbbb \comment{pred-2}
\end{schema}
\nextside
\begin{zpar}
This is a paragraph which has the same
margins as the standard schemas do.
\end{zpar}
\end{sidebyside}
\verbpart
\begin{sidebyside}
\begin{schema}{Schema}
\comment*{declarations}
\ST
a < b \comment{pred-1} \\
aaaaa < bbbbb \comment{pred-2}
\end{schema}
\nextside
\begin{zpar}
This is a paragraph which has the same
margins as the standard schemas do.
\end{zpar}
\end{sidebyside}
\end{verbatim}
\end{example}

In fact, this environment was used throughout this note to
display the examples beside the required input text.
Incidentally, the above example shows that \verb|sidebyside|
environments can be nested; so what the author of this note typed
to get the above display was:

\begin{quote}
\begin{verbatim}
\begin{sidebyside}
        \begin{sidebyside}
                ...
        \nextside
                ...
        \end{sidebyside}
\nextside
        ...
\end{sidebyside}
\end{verbatim}
\end{quote}

This resulted in the first two columns being equally spaced and
together taking up as much space as the third column.
You can have more than 2 columns without nesting by specifying an optional
parameter to \verb|sidebyside|.  For example, the display below has three
equally spaced columns obtained using \verb|\begin{sidebyside}[3]|.
\begin{sidebyside}[3]
\begin{schema}{BirthdayBook}
    known: \pset NAME \\
    birthday: NAME \pfun DATE
\ST
    known = \dom birthday
\end{schema}
\nextside
\begin{schema}{BirthdayBook}
    known: \pset NAME \\
    birthday: NAME \pfun DATE
\ST
    known = \dom birthday
\end{schema}
\nextside
\begin{zpar}
Don't get carried away with \verb|sidebyside|
like this example does.
\end{zpar}
\end{sidebyside}
\newpage
\section{Style Parameters}

\begin{description}
\item[\tt\string\zedindent] The (horizontal) indentation for mathematical text.
	By default, this is the same as \verb|\leftmargini|, the indentation
	used for list environments.
\item[\tt\string\zedleftsep] The (horizontal) space between the vertical line on the left
	of schemas, etc., and the maths inside. The default is 1em.
\item[\tt\string\zedtab] The unit of indentation used by \verb|\t|. The default
	is 2em.
\item[\tt\string\zedbar] The length of the horizontal bar in the middle of a
	schema. The default is 8em.
\item[\tt\string\leftschemas] A declaration which makes schema names be
	set flush left. Use it in the document preamble.
\item[\tt\string\zedlinethickness] The thickness of the lines that make up
	schema and class boxes.  You can change the thickness
	with a command such as \verb|\zedlinethickness=0.1pt|.  This may
	be useful if you are creating overhead slides.
	\begin{description}
	\makeatletter
	\item[0.1pt] \zedlinethickness=0.1pt
		~\hbox to 4cm{\z@hrulefill}
	\item[0.4pt] \zedlinethickness=0.4pt
		~\hbox to 4cm{\z@hrulefill}~~~(The default)
	\item[\hphantom{0.}1pt] \zedlinethickness=1pt
		~\hbox to 4cm{\z@hrulefill}
	\end{description}
\item[\tt\string\baselinestretch] The spacing for the text part of your
	document.  It doesn't change the spacing within Z environments.  It's
	default value is 1.  A command such as \verb|\def\baselinestretch{2}|
	will make your text double spaced, but not your Z environments.
\item[\tt\string\zedbaselinestretch] The spacing for the Z environment
	part of your document.  It's default value is 1.
\item[\tt\string\zedsize] The size of the material within the Z
	part of your document. It doesn't affect the remainder of your document.
	For example, \verb|\zedsize{\large}| will give you large Z symbols
	and equations but will not affect the size of the surrounding text.
\item[\tt\string\zedcornerheight] The height of `corners' that can be placed
	on the right hand side of the top and bottom lines of schema and class
	boxes.  The default is 0em (i.e. no corners).
\end{description}

\section{Symbols}

Multi-letter identifiers have been changed to look
better than they do with vanilla \LaTeX: instead of
$\mit specifications$, you get $specifications$.
The letters haven't been spread apart, and the
ligature $fi$ has been used.

Almost all of the mathematical symbols of \LaTeX\ can be used;
some have been redefined---usually to fix the spacing so that it is
suitable for Z specifications.
The commands for obtaining additional symbols are listed below.
Sometimes more than one command may produce a symbol you
require.  You should use the one that seems to be designed for the
context you have in mind.  This is because the spacing around (and size of)
symbols has been chosen for their typical context.

Throughout the lifetime of these macros a number of alternate control
sequences for any symbol may have existed.  A list of aliases has been
set up so that old commands may still be used.  It is
recommended however that you stick to the recommended command
names for symbols as these names may be supported by other tools.
Within the table below non-recommended aliases are surrounded by
brackets, e.g., \verb|(\power)|.
\threecolumn
\setcounter{secnumdepth}{2}
\zedindent=0.2\zedindent
\subsection{Special Z Notation}
\vspace*{-0.5ex}
\subsubsection{Numbers}
\vspace*{-2.5ex}
\begin{symbols}
\nat & \verb' \nat' \\
\natone & \verb' \natone (\nplus)' \\
\integer & \verb' \integer (\num)' \\
\real & \verb' \real' \\
\div~\mod & \verb' \div \mod' \\
i^n & \verb' i^n i\expon n' \\
\succ & \verb' \succ' \\
%\prec & \verb' \prec' \\
=~\neq & \verb' = \neq' \\
<~\leq~\leqslant & \verb' < \leq \leqslant' \\
>~\geq~\geqslant & \verb' > \geq \geqslant' \\
*\,/\,+ - & \verb' * / + -' \\
\end{symbols}
\subsubsection{Logic}
\vspace*{-2.5ex}
\begin{symbols}
\lnot & \verb'\lnot' \\
\land & \verb'\land (\wedge)' \\
\lor & \verb'\lor (\vee)' \\
\all & \verb'\all (\forall)' \\
\exi & \verb'\exi (\exists)' \\
\exi_1 & \verb'\exione' \\
\nexi & \verb'\nexi (\nexists)' \\
\dot & \verb'@ \dot (\spot)' \\
%\cond & \verb'\cond' \\
\imp & \verb'\imp (\implies)' \\
\iff & \verb'\iff' \\
\true & \verb'\true' \\
\false & \verb'\false' \\
\bool & \verb'\bool' \\
\end{symbols}
\subsubsection{Sets}
\vspace*{-2.5ex}
\begin{symbols}
\{~~\cbar~~\} & \verb' \{ \cbar \}' \\
\emptyset & \verb' \emptyset' \\
\varemptyset & \verb' \varemptyset' \\
\mem & \verb' \mem (\in)' \\
\nmem & \verb' \nem (\nmem \notin)' \\
\pset & \verb' \pset (\power)' \\
\fset & \verb' \fset (\finset)' \\
\psetone~~\fsetone & \verb' \fsetone \psetone' \\
\uni & \verb' \uni (\union)' \\
\int & \verb' \int (\inter)' \\
\psubs & \verb' \psubs (\subset)' \\
\subs & \verb' \subs (\subseteq)' \\
\psups & \verb' \psups (\supset)' \\
\sups & \verb' \sups (\supseteq)' \\
\prod & \verb' \prod (\cross)' \\
\min~\max & \verb' \min \max' \\
\# & \verb' \#' \\
\duni & \verb' \duni (\dunion)' \\
\dint & \verb' \dint (\dinter)' \\
\upto & \verb' \upto' \\
\end{symbols}

\subsubsection{Relations and Functions}
\vspace*{-2.5ex}
\begin{symbols}[0.1]
\lambda~~~\mu & \verb'\lambda \mu' \\
\dom & \verb'\dom' \\
\ran & \verb'\ran' \\
\dres & \verb'\dres' \\
\dsub & \verb'\dsub (\ndres)' \\
\rres & \verb'\rres' \\
\rsub & \verb'\rsub (\nrres)' \\
\fovr & \verb'\fovr' \\
\cmp & \verb'\cmp' \\
\fcmp & \verb'\fcmp (\comp)' \\
(\!|~~~|\!) & \verb'\limg \rimg' \\
\id & \verb'\id' \\
R\inv & \verb'R^{-1}  R\inv' \\
R^+ &   \verb'R^+     R\tcl' \\
R^* &   \verb'R^*     R\rtcl' \\
R^k &   \verb'R^k     R\iter k' \\
iter\,0\,R & \verb'iter \, 0 \, R' \\
\map & \verb'\map' \\
\rel & \verb'\rel' \\
\tfun & \verb'\tfun (\fun)' \\
\tinj & \verb'\tinj (\inj)' \\
\tsur & \verb'\tsur (\surj)' \\
\pfun & \verb'\pfun' \\
\pinj & \verb'\pinj' \\
\psur & \verb'\psur (\psurj)' \\
\ffun & \verb'\ffun' \\
\finj & \verb'\finj' \\
\bij & \verb'\bij' \\
\end{symbols}
\subsubsection{Sequences}
\vspace*{-2.5ex}
\begin{symbols}
\seq & \verb'   \seq' \\
\seqone & \verb'   \seqone' \\
\emptyseq & \verb'   \emptyseq' \\
\lseq~~~\rseq & \verb'   \lseq \rseq' \\
\head~~\tail & \verb'   \head \tail' \\
\front~~\last & \verb'   \front \last' \\
\rev & \verb'   \rev' \\
\next & \verb'   \next' \\
\inseq & \verb'   \inseq' \\
\prefix & \verb'   \prefix' \\
\suffix & \verb'   \suffix' \\
\squash & \verb'   \squash' \\
\cat & \verb'   \cat' \\
\dcat & \verb'   \dcat' \\
\dcmp & \verb'   \dcmp' \\
\dovr & \verb'   \dovr' \\
\ires & \verb'   \ires' \\
\sres & \verb'   \sres \filter' \\
\partitions & \verb'   \partitions' \\
\disjoint & \verb'   \disjoint' \\
\end{symbols}

\subsubsection{Schemas}
\vspace*{-2.5ex}
\begin{symbols}
\Delta & \verb'\Delta' \\
\equiv~~\Xi & \verb'\equiv \Xi' \\
\pred & \verb'\pred' \\
\pre & \verb'\pre' \\
\post & \verb'\post' \\
\project & \verb'\zproject \project' \\
\zand & \verb'\zand' \\
\zor & \verb'\zor' \\
\zcmp & \verb'\zcmp (\semi)' \\
\zexi & \verb'\zexi' \\
\zall & \verb'\zall' \\
\znot & \verb'\znot' \\
\zhide & \verb'\zhide (\hide)' \\
\zfor & \verb'\zfor' \\
\zimp & \verb'\zimp' \\
\zeq & \verb'\zeq' \\
\zovr & \verb'\zovr' \\
\zpipe & \verb'\zpipe' \\
\theta & \verb'\theta' \\
\lsch~~\zbar~~\rsch & \verb'\lsch \zbar \rsch' \\
. & \verb'.' \\
\end{symbols}
\subsubsection{Bags}
\vspace*{-2.5ex}
\begin{symbols}
\lbag~~~\rbag & \verb'\lbag \rbag' \\
\bag & \verb'\bag' \\
\emptybag & \verb'\emptybag' \\
\items & \verb'\items' \\
\bagcount & \verb'\bagcount' \\
\buni & \verb'\buni' \\
\inbag & \verb'\inbag' \\
\end{symbols}
\subsubsection{Definitions and Declarations}
\vspace*{-2.5ex}
\begin{symbols}
::= & \verb'\ddef' \\
\bbar & \verb'\bbar' \\
== & \verb'\defs' \also
\widehat= & \verb'\sdef' \also
\triangleq & \verb'\varsdef' \\
,~~\semicolon~~: & \verb', ; :' \\
\lang~~~\rang & \verb'\lang \rang' \\
\end{symbols}
\subsubsection{Miscellaneous}
\vspace*{-2.5ex}
\begin{symbols}[0]
[~~~] & \verb'[ ]' \\
(~~~) & \verb'( )' \\
!~~~? & \verb'! ?' \\
\zlet & \verb'\zlet' \\
\zwhere & \verb'\zwhere' \\
\zin & \verb'\zin' \\
\langle\!|~~~|\!\rangle & \verb'\lblot \rblot' \\
\intern Bump & \verb'\intern Bump' \\
\Init & \verb'\Init'\\
\Exit & \verb'\Exit'
\end{symbols}

\subsection{Other Special Notation}
\vspace*{-1ex}
\subsubsection{Temporal Logic}
\vspace*{-2.5ex}
\begin{symbols}
\always~\uptilnow & \verb'\always \uptilnow' \\
~&\verb'(\henceforth)'\\
\atnext~\atlast & \verb'\atnext \atlast' \\
\eventually~\previously & \verb'\eventually \previously' \\
\end{symbols}
\subsubsection{Proofs}
\vspace*{-2.5ex}
\begin{symbols}[0.1]
\TH & \verb'   \TH' \\
\PR & \verb'   \PR' \\
\LE & \verb'   \LE' \\
\ETH~\Qed & \verb'   \qed (\ETH) \Qed' \\
\QED~\BLACKQED & \verb'   \QED \BLACKQED' \\
\vdash & \verb'   \shows (\thrm)' \\
\vDash & \verb'   \vDash' \\
\refines & \verb'   \refines' \\
\weakrefine & \verb'   \weakrefine' \\
\end{symbols}
\subsubsection{Object Theory}
\vspace*{-2.5ex}
\begin{symbols}
\subclass & \verb'\subclass \isa' \\
\weaksubclass & \verb'\weaksubclass \islikea' \\
\supclass & \verb'\supclass' \\
\weaksupclass & \verb'\weaksupclass' \\
\hasa & \verb'\hasa \instantiates' \\
\instancein & \verb'\instancein' \\
\subtype~~\subtypeeq & \verb'\subtype \subtypeeq' \\
\suptype~~\suptypeeq & \verb'\suptype \suptypeeq' \\
\end{symbols}
\subsubsection{Orders}
\vspace*{-2.5ex}
\begin{symbols}
\mono & \verb'      \mono' \\ % these lines fudged to give more spacing
\torder & \verb'      \torder' \\
\porder & \verb'      \porder' \\
\end{symbols}
\subsubsection{Word Styles}
\vspace*{-2.5ex}
\begin{symbols}[0.4]
\word{word} & \verb'\word{word}' \\
\keyword{word} & \verb'\keyword{word}' \\
\boldword{word} & \verb'\boldword{word}' \\
\underword{word} & \verb'\underword{word}' \\
\underkeyword{word} & \verb'\underkeyword{word}' \\
\underboldword{word} & \verb'\underboldword{word}' \\
\String{word} & \verb'\String{word}' \\
\STRING{word} & \verb'\STRING{word}' \\
a \infix{rel} b & \verb'a \infix{rel} b' \\
\end{symbols}

\subsection{Special Letter Fonts}
\vspace*{-1ex}
\subsubsection{Greek}
\vspace*{-2.5ex}
\begin{symbols}
\alpha & \verb'\alpha' \\
\beta & \verb'\beta' \\
\gamma~\Gamma & \verb'\gamma \Gamma' \\
\delta~\Delta & \verb'\delta \Delta' \\
\epsilon~\varepsilon & \verb'\epsilon \varepsilon' \\
\zeta & \verb'\zeta' \\
\eta & \verb'\eta' \\
\theta~\vartheta~\Theta & \verb'\theta \vartheta \Theta' \\
\iota & \verb'\iota' \\
\kappa~\varkappa & \verb'\kappa \varkappa' \\
\lambda~\Lambda & \verb'\lambda \Lambda' \\
\mu & \verb'\mu' \\
\nu & \verb'\nu' \\
\xi~\Xi & \verb'\xi \Xi' \\
\pi~\varpi~\Pi & \verb'\pi \varpi \Pi' \\
\rho~\varrho & \verb'\rho \varrho' \\
\sigma~\varsigma~\Sigma & \verb'\sigma \varsigma \Sigma' \\
\tau & \verb'\tau' \\
\upsilon~\Upsilon & \verb'\upsilon \Upsilon' \\
\phi~\varphi~\Phi & \verb'\phi \varphi \Phi' \\
\chi & \verb'\chi' \\
\psi~\Psi & \verb'\psi \Psi' \\
\omega~\Omega & \verb'\omega \Omega' \\
\end{symbols}
\subsubsection{Caligraphic}
\vspace*{-2.5ex}
\begin{symbols}
\cal A & \verb'\cal A' \\
\cal B & \verb'\cal B' \\
\cal C & \verb'\cal C' \\
\cal D & \verb'\cal D' \\
\cal E & \verb'\cal E' \\
\cal F & \verb'\cal F' \\
\cal G & \verb'\cal G' \\
\cal H & \verb'\cal H' \\
\cal I & \verb'\cal I' \\
\cal J & \verb'\cal J' \\
\cal K & \verb'\cal K' \\
\cal L & \verb'\cal L' \\
\cal M & \verb'\cal M' \\
\cal N & \verb'\cal N' \\
\cal O & \verb'\cal O' \\
\cal P & \verb'\cal P' \\
\cal Q & \verb'\cal Q' \\
\cal R & \verb'\cal R' \\
\cal S & \verb'\cal S' \\
\cal T & \verb'\cal T' \\
\cal U & \verb'\cal U' \\
\cal V & \verb'\cal V' \\
\cal W & \verb'\cal W' \\
\cal X & \verb'\cal X' \\
\cal Y & \verb'\cal Y' \\
\cal Z & \verb'\cal Z' \\
\end{symbols}
\subsubsection{BlackBoard Bold}
\vspace*{-2.5ex}
\begin{symbols}
\bbold A & \verb'\bbold A' \\
\bbold B & \verb'\bbold B' \\
\bbold C & \verb'\bbold C' \\
\bbold D & \verb'\bbold D' \\
\bbold E & \verb'\bbold E' \\
\bbold F & \verb'\bbold F' \\
\bbold G & \verb'\bbold G' \\
\bbold H & \verb'\bbold H' \\
\bbold I & \verb'\bbold I' \\
\bbold J & \verb'\bbold J' \\
\bbold K & \verb'\bbold K' \\
\bbold L & \verb'\bbold L' \\
\bbold M & \verb'\bbold M' \\
\bbold N & \verb'\bbold N' \\
\bbold O & \verb'\bbold O' \\
\bbold P & \verb'\bbold P' \\
\bbold Q & \verb'\bbold Q' \\
\bbold R & \verb'\bbold R' \\
\bbold S & \verb'\bbold S' \\
\bbold T & \verb'\bbold T' \\
\bbold U & \verb'\bbold U' \\
\bbold V & \verb'\bbold V' \\
\bbold W & \verb'\bbold W' \\
\bbold X & \verb'\bbold X' \\
\bbold Y & \verb'\bbold Y' \\
\bbold Z & \verb'\bbold Z' \\
\end{symbols}
\subsubsection{Miscellaneous}
\vspace*{-2.5ex}
\begin{symbols}
\hslash & \verb'\hslash' \\
\hbar & \verb'\hbar' \\
\backepsilon & \verb'\backepsilon' \\
\eth & \verb'\eth' \\
\beth & \verb'\beth' \\
\gimel & \verb'\gimel' \\
\daleth & \verb'\daleth' \\
\complement & \verb'\complement' \\
\intercal & \verb'\intercal' \\
\aleph & \verb'\aleph' \\
\nabla & \verb'\nabla' \\
\hbar & \verb'\hbar' \\
\imath & \verb'\imath' \\
\jmath & \verb'\jmath' \\
\ell & \verb'\ell' \\
\wp & \verb'\wp' \\
\Re & \verb'\Re' \\
\Im & \verb'\Im' \\
\mho & \verb'\mho' \\
\digamma & \verb'\digamma' \\
\end{symbols}

\subsection{Shapes}
\vspace*{-2ex}
\begin{symbols}
\Box & \verb'\Box' \\
\square & \verb'\square' \\
\blacksquare & \verb'\blacksquare' \\
\diamond & \verb'\diamond' \\
\Diamond & \verb'\Diamond' \\
\lozenge & \verb'\lozenge' \\
\blacklozenge & \verb'\blacklozenge' \\
\vartriangleright & \verb'\vartriangleright' \\
\vartriangleleft & \verb'\vartriangleleft' \\
\blacktriangledown & \verb'\blacktriangledown' \\
\blacktriangleright & \verb'\blacktriangleright' \\
\blacktriangleleft & \verb'\blacktriangleleft' \\
\vartriangle & \verb'\vartriangle' \\
\blacktriangle & \verb'\blacktriangle' \\
\triangledown & \verb'\triangledown' \\
\triangle & \verb'\triangle' \\
\triangleleft & \verb'\triangleleft' \\
\triangleright & \verb'\triangleright' \\
\bigtriangleup & \verb'\bigtriangleup' \\
\bigtriangledown & \verb'\bigtriangledown' \\
\clubsuit & \verb'\clubsuit' \\
\diamondsuit & \verb'\diamondsuit' \\
\heartsuit & \verb'\heartsuit' \\
\spadesuit & \verb'\spadesuit' \\
\ast & \verb'\ast' \\
\star & \verb'\star' \\
\maltese & \verb'\maltese' \\
\bigstar & \verb'\bigstar' \\
\bigcirc & \verb'\bigcirc' \\
\circ & \verb'\circ' \\
\bullet & \verb'\bullet' \\
\centerdot & \verb'\centerdot' \\
\cdot & \verb'\cdot' \\
\cdots & \verb'\cdots' \\
\ldots & \verb'\ldots' \\
\vdots & \verb'\vdots' \\
\ddots & \verb'\ddots' \\
\end{symbols}
\subsubsection{Circled Operations}
\vspace*{-2.5ex}
\begin{symbols}
\circledS & \verb'\circledS' \\
\circledcirc & \verb'\circledcirc' \\
\circledast & \verb'\circledast' \\
\circleddash & \verb'\circleddash' \\
\circledR & \verb'\circledR' \\
\copyright & \verb'\copyright' \\
\fovr & \verb'\fovr' \\
\ominus & \verb'\ominus' \\
\otimes & \verb'\otimes' \\
\oslash & \verb'\oslash' \\
\odot & \verb'\odot' \\
\end{symbols}

\subsubsection{Boxed operators}
\vspace*{-2.5ex}
\begin{symbols}[0.2]
\boxdot & \verb'\boxdot' \\
\boxplus & \verb'\boxplus' \\
\boxtimes & \verb'\boxtimes' \\
\boxminus & \verb'\boxminus' \\
\end{symbols}
\subsection{Arrow Symbols}
\vspace*{-1ex}
\subsubsection{Left Arrows}
\vspace*{-2.5ex}
\begin{symbols}[0.7]
\leftarrow & \verb'\leftarrow	\gets' \\
\Leftarrow & \verb'\Leftarrow' \\
\hookleftarrow & \verb'\hookleftarrow' \\
\leftharpoonup & \verb'\leftharpoonup' \\
\leftharpoondown & \verb'\leftharpoondown' \\
\longleftarrow & \verb'\longleftarrow' \\
\Longleftarrow & \verb'\Longleftarrow' \\
\twoheadleftarrow & \verb'\twoheadleftarrow' \\
\leftleftarrows & \verb'\leftleftarrows' \\
\leftarrowtail & \verb'\leftarrowtail' \\
\Lleftarrow & \verb'\Lleftarrow' \\
\nleftarrow & \verb'\nleftarrow' \\
\nLeftarrow & \verb'\nLeftarrow' \\
\end{symbols}

\subsubsection{Right Arrows}
\begin{symbols}[0.7]
\rightarrow & \verb'\rightarrow	\to' \\
\Rightarrow & \verb'\Rightarrow' \\
\map & \verb'\map' \\
\longmapsto & \verb'\longmapsto' \\
\hookrightarrow & \verb'\hookrightarrow' \\
\rightharpoonup & \verb'\rightharpoonup' \\
\rightharpoondown & \verb'\rightharpoondown' \\
\leadsto & \verb'\leadsto' \\
\longrightarrow & \verb'\longrightarrow' \\
\Longrightarrow & \verb'\Longrightarrow' \\
\twoheadrightarrow & \verb'\twoheadrightarrow' \\
\rightrightarrows & \verb'\rightrightarrows' \\
\rightarrowtail & \verb'\rightarrowtail' \\
\rightsquigarrow & \verb'\rightsquigarrow' \\
\Rrightarrow & \verb'\Rrightarrow' \\
\nrightarrow & \verb'\nrightarrow' \\
\nRightarrow & \verb'\nRightarrow' \\
\end{symbols}
\newpage
\subsubsection{Left Right Arrows}
\begin{symbols}[0.6]
\leftrightarrow & \verb'\leftrightarrow' \\
\Leftrightarrow & \verb'\Leftrightarrow' \\
\rightleftharpoons & \verb'\rightleftharpoons' \\
\longleftrightarrow & \verb'\longleftrightarrow' \\
\Longleftrightarrow & \verb'\Longleftrightarrow' \\
\rightleftharpoons & \verb'\rightleftharpoons' \\
\leftrightharpoons & \verb'\leftrightharpoons' \\
\leftrightarrows & \verb'\leftrightarrows' \\
\rightleftarrows & \verb'\rightleftarrows' \\
\leftrightsquigarrow & \verb'\leftrightsquigarrow' \\
\nLeftrightarrow & \verb'\nLeftrightarrow' \\
\nleftrightarrow & \verb'\nleftrightarrow' \\
\end{symbols}

\subsubsection{Up Down Arrows}
\begin{symbols}[1]
\uparrow & \verb'\uparrow' \\
\Uparrow & \verb'\Uparrow' \\
\downarrow & \verb'\downarrow' \\
\Downarrow & \verb'\Downarrow' \\
\updownarrow & \verb'\updownarrow' \\
\Updownarrow & \verb'\Updownarrow' \\
\upuparrows & \verb'\upuparrows' \\
\downdownarrows & \verb'\downdownarrows' \\
\upharpoonright & \verb'\upharpoonright' \\
\downharpoonright & \verb'\downharpoonright' \\
\upharpoonleft & \verb'\upharpoonleft' \\
\downharpoonleft & \verb'\downharpoonleft' \\
\end{symbols}

\subsubsection{Miscellaneous}
\begin{symbols}[0.9]
\nearrow & \verb'\nearrow' \\
\searrow & \verb'\searrow' \\
\swarrow & \verb'\swarrow' \\
\nwarrow & \verb'\nwarrow' \\
\circlearrowright & \verb'\circlearrowright' \\
\circlearrowleft & \verb'\circlearrowleft' \\
\Lsh & \verb'\Lsh' \\
\Rsh & \verb'\Rsh' \\
\looparrowleft & \verb'\looparrowleft' \\
\looparrowright & \verb'\looparrowright' \\
\curvearrowleft & \verb'\curvearrowleft' \\
\curvearrowright & \verb'\curvearrowright' \\
\end{symbols}
\pagebreak[4]

\subsection{Relations}
\begin{symbols}[0.8]
\ll & \verb'\ll' \\
\gg & \verb'\gg' \\
\llless & \verb'\lll \llless' \\
\gggtr & \verb'\ggg \gggtr' \\
\sqsubset & \verb'\sqsubset' \\
\sqsupset & \verb'\sqsupset' \\
\sqsubseteq & \verb'\sqsubseteq' \\
\sqsupseteq & \verb'\sqsupseteq' \\
\owns & \verb'\owns' \\
\vdash & \verb'\vdash' \\
\Vdash & \verb'\Vdash' \\
\vDash & \verb'\vDash' \\
\dashv & \verb'\dashv' \\
\Vvdash & \verb'\Vvdash' \\
\models & \verb'\models' \\
\nvdash & \verb'\nvdash' \\
\nVdash & \verb'\nVdash' \\
\nvDash & \verb'\nvDash' \\
\nVDash & \verb'\nVDash' \\
\perp & \verb'\perp' \\
\sim & \verb'\sim' \\
\simeq & \verb'\simeq' \\
\eqsim & \verb'\eqsim' \\
\backsim & \verb'\backsim' \\
\backsimeq & \verb'\backsimeq' \\
\thicksim & \verb'\thicksim' \\
\nsim & \verb'\nsim' \\
\approx & \verb'\approx' \\
\napprox & \verb'\napprox' \\
\thickapprox & \verb'\thickapprox' \\
\approxeq & \verb'\approxeq' \\
\asymp & \verb'\asymp' \\
\cong & \verb'\cong' \\
\ncong & \verb'\ncong' \\
\doteq & \verb'\doteq' \\
\doteqdot & \verb'\Doteq \doteqdot' \\
\risingdotseq & \verb'\risingdotseq' \\
\fallingdotseq & \verb'\fallingdotseq' \\
\lessdot & \verb'\lessdot' \\
\gtrdot & \verb'\gtrdot' \\
\eqcirc & \verb'\eqcirc' \\
\circeq & \verb'\circeq' \\
\bumpeq & \verb'\bumpeq' \\
\Bumpeq & \verb'\Bumpeq' \\
\triangleq & \verb'\triangleq' \\
\multimap & \verb'\multimap' \\
\propto & \verb'\propto' \\
\varpropto & \verb'\varpropto' \\
\lesssim & \verb'\lesssim' \\
\gtrsim & \verb'\gtrsim' \\
\lessapprox & \verb'\lessapprox' \\
\gtrapprox & \verb'\gtrapprox' \\
\xprec & \verb'\xprec' \\
\xsucc & \verb'\xsucc' \\
\preceq & \verb'\preceq' \\
\succeq & \verb'\succeq' \\
\precsim & \verb'\precsim' \\
\succsim & \verb'\succsim' \\
\precapprox & \verb'\precapprox' \\
\succapprox & \verb'\succapprox' \\
\eqslantless & \verb'\eqslantless' \\
\eqslantgtr & \verb'\eqslantgtr' \\
\curlyeqprec & \verb'\curlyeqprec' \\
\curlyeqsucc & \verb'\curlyeqsucc' \\
\preccurlyeq & \verb'\preccurlyeq' \\
\succcurlyeq & \verb'\succcurlyeq' \\
\leqq & \verb'\leqq' \\
\geqq & \verb'\geqq' \\
\leqslant & \verb'\leqslant' \\
\geqslant & \verb'\geqslant' \\
\lessgtr & \verb'\lessgtr' \\
\gtrless & \verb'\gtrless' \\
\lesseqgtr & \verb'\lesseqgtr' \\
\Also
\gtreqless & \verb'\gtreqless' \\
\Also
\lesseqqgtr & \verb'\lesseqqgtr' \\
\Also
\gtreqqless & \verb'\gtreqqless' \\
\also
\lvertneqq & \verb'\lvertneqq' \\
\gvertneqq & \verb'\gvertneqq' \\
\nleq & \verb'\nleq' \\
\ngeq & \verb'\ngeq' \\
\nless & \verb'\nless' \\
\ngtr & \verb'\ngtr' \\
\nprec & \verb'\nprec' \\
\nsucc & \verb'\nsucc' \\
\lneqq & \verb'\lneqq' \\
\gneqq & \verb'\gneqq' \\
\nleqslant & \verb'\nleqslant' \\
\ngeqslant & \verb'\ngeqslant' \\
\lneq & \verb'\lneq' \\
\gneq & \verb'\gneq' \\
\npreceq & \verb'\npreceq' \\
\nsucceq & \verb'\nsucceq' \\
\precnsim & \verb'\precnsim' \\
\succnsim & \verb'\succnsim' \\
\lnsim & \verb'\lnsim' \\
\gnsim & \verb'\gnsim' \\
\nleqq & \verb'\nleqq' \\
\ngeqq & \verb'\ngeqq' \\
\precneqq & \verb'\precneqq' \\
\succneqq & \verb'\succneqq' \\
\precnapprox & \verb'\precnapprox' \\
\succnapprox & \verb'\succnapprox' \\
\lnapprox & \verb'\lnapprox' \\
\gnapprox & \verb'\gnapprox' \\
\Subset & \verb'\Subset' \\
\Supset & \verb'\Supset' \\
\subseteqq & \verb'\subseteqq' \\
\supseteqq & \verb'\supseteqq' \\
%\varsubsetneq & \verb'\varsubsetneq' \\
%\varsupsetneq & \verb'\varsupsetneq' \\
\nsubseteqq & \verb'\nsubseteqq' \\
\also
\nsupseteqq & \verb'\nsupseteqq' \\
\also
\subsetneqq & \verb'\subsetneqq' \\
\also
\supsetneqq & \verb'\supsetneqq' \\
%\varsubsetneqq & \verb'\varsubsetneqq' \\
%\varsupsetneqq & \verb'\varsupsetneqq' \\
\subsetneq & \verb'\subsetneq' \\
\supsetneq & \verb'\supsetneq' \\
\nsubseteq & \verb'\nsubseteq' \\
\nsupseteq & \verb'\nsupseteq' \\
\trianglerighteq & \verb'\trianglerighteq' \\
\trianglelefteq & \verb'\trianglelefteq' \\
\ntrianglerighteq & \verb'\ntrianglerighteq' \\
\ntrianglelefteq & \verb'\ntrianglelefteq' \\
\ntriangleleft & \verb'\ntriangleleft' \\
\ntriangleright & \verb'\ntriangleright' \\
\between & \verb'\between' \\
| & \verb'| \vert \mid' \\
\| & \verb'\| \Vert \parallel' \\
\interleave & \verb'\interleave' \\
\shortmid & \verb'\shortmid' \\
\shortparallel & \verb'\shortparallel' \\
\shortinterleave & \verb'\shortinterleave' \\
\nparallel & \verb'\nparallel' \\
\nmid & \verb'\nmid' \\
\nshortmid & \verb'\nshortmid' \\
\nshortparallel & \verb'\nshortparallel' \\
\end{symbols}

\subsection{Binary Operations}
\begin{symbols}[1.4]
\curlywedge & \verb'\curlywedge' \\
\curlyvee & \verb'\curlyvee' \\
\veebar & \verb'\veebar' \\
\barwedge & \verb'\barwedge' \\
\doublebarwedge & \verb'\doublebarwedge' \\
\pm & \verb'\pm' \\
\mp & \verb'\mp' \\
\times & \verb'\times' \\
\ltimes & \verb'\ltimes' \\
\rtimes & \verb'\rtimes' \\
\leftthreetimes & \verb'\leftthreetimes' \\
\rightthreetimes & \verb'\rightthreetimes' \\
\divideontimes & \verb'\divideontimes' \\
\divides & \verb'\divides' \\
\uplus & \verb'\uplus' \\
\sqcap & \verb'\sqcap' \\
\sqcup & \verb'\sqcup' \\
\Cup & \verb'\Cup \doublecup' \\
\Cap & \verb'\Cap \doublecap' \\
\backslash & \verb'\backslash' \\
\setminus & \verb'\setminus' \\
\smallsetminus & \verb'\smallsetminus' \\
\wr & \verb'\wr' \\
\lhd & \verb'\lhd' \\
\rhd & \verb'\rhd' \\
\unlhd & \verb'\unlhd' \\
\unrhd & \verb'\unrhd' \\
\restriction & \verb'\restriction' \\
\amalg & \verb'\amalg' \\
\top & \verb'\top' \\
\bot & \verb'\bot' \\
\smallsmile & \verb'\smallsmile' \\
\smallfrown & \verb'\smallfrown' \\
\smile & \verb'\smile' \\
\frown & \verb'\frown' \\
\pitchfork & \verb'\pitchfork' \\
\dotplus & \verb'\dotplus' \\
\Join & \verb'\Join' \\
\bowtie & \verb'\bowtie' \\
\end{symbols}

\subsection{Miscellaneous Symbols}
\begin{symbols}
\dagger & \verb'\dagger' \\
\ddagger & \verb'\ddagger' \\
\sectionsymbol & \verb'\sectionsymbol' \\
\P & \verb'\P' \\
\angle & \verb'\angle' \\
\measuredangle & \verb'\measuredangle' \\
\sphericalangle & \verb'\sphericalangle' \\
\prime & \verb'\prime' \\
\backprime & \verb'\backprime' \\
\surd & \verb'\surd' \\
\smallint & \verb'\smallint' \\
\flat & \verb'\flat' \\
\natural & \verb'\natural' \\
\sharp & \verb'\sharp' \\
\partial & \verb'\partial' \\
\infty & \verb'\infty' \\
\yen & \verb'\yen' \\
\therefore & \verb'\therefore' \\
\because & \verb'\because' \\
\checkmark & \verb'\checkmark' \\
\end{symbols}

\subsection{Variable-sized Symbols}
These symbols come in two sizes which
do not vary with the point size of your
font.  The big size can be obtained
by preceding the symbol command with
the command \verb'\displaystyle'.
\begin{symbols}[1.3]
\sum \displaystyle \sum & \verb'\sum' \\
\product \displaystyle \product & \verb'\product' \\
\coprod \displaystyle \coprod & \verb'\coprod' \\
\integral \displaystyle \integral & \verb'\integral' \\
\oint \displaystyle \oint & \verb'\oint' \\
\bigcap \displaystyle \bigcap & \verb'\bigcap' \\
\bigcup \displaystyle \bigcup & \verb'\bigcup' \\
\bigsqcup \displaystyle \bigsqcup & \verb'\bigsqcup' \\
\bigvee \displaystyle \bigvee & \verb'\bigvee' \\
\bigwedge \displaystyle \bigwedge & \verb'\bigwedge' \\
\bigodot \displaystyle \bigodot & \verb'\bigodot' \\
\bigotimes \displaystyle \bigotimes & \verb'\bigotimes' \\
\bigoplus \displaystyle \bigoplus & \verb'\bigoplus' \\
\biguplus \displaystyle \biguplus & \verb'\biguplus' \\
\end{symbols}

\subsection{Delimiters}
\vspace*{-1ex}
These symbols can be made large to surround large formula.
E.g., $$\left\lfloor\displaystyle\sum_{i=1}^n x^i\right\rfloor$$
was generated using

\begin{verbatim}
\left\lfloor...\right\rfloor
\end{verbatim}
\vspace*{-2ex}
\begin{symbols}[0.8]
(~~~) & \verb'( )' \\
\{~~~\} & \verb'\{ \}' \\
\lfloor~~~\rfloor & \verb'\lfloor \rfloor' \\
\lceil~~~\rceil & \verb'\lceil \rceil' \\
\langle~~~\rangle & \verb'\langle \rangle' \\
\ulcorner~~~\urcorner & \verb'\ulcorner \urcorner' \\
\llcorner~~~\lrcorner & \verb'\llcorner \lrcorner' \\
\uparrow & \verb'\uparrow' \\
\downarrow & \verb'\downarrow' \\
\updownarrow & \verb'\updownarrow' \\
\Uparrow & \verb'\Uparrow' \\
\Downarrow & \verb'\Downarrow' \\
\Updownarrow & \verb'\Updownarrow' \\
\end{symbols}

\subsection{Math Accents}
\vspace*{-1ex}
\begin{symbols}[0.2]
\hat{a} & \verb'\hat{a}' \\
\widehat{a} & \verb'\widehat{a}' \\
\widehat{aa} & \verb'\widehat{aa}' \\
\widehat{aaa} & \verb'\widehat{aaa}' \\
\tilde{a} & \verb'\tilde{a}' \\
\widetilde{a} & \verb'\widetilde{a}' \\
\widetilde{aa} & \verb'\widetilde{aa}' \\
\widetilde{aaa} & \verb'\widetilde{aaa}' \\
\check{a} & \verb'\check{a}' \\
\breve{a} & \verb'\breve{a}' \\
\acute{a} & \verb'\acute{a}' \\
\grave{a} & \verb'\grave{a}' \\
\bar{a} & \verb'\bar{a}' \\
\vec{a} & \verb'\vec{a}' \\
\dotaccent{a} & \verb'\dotaccent{a}' \\
\ddot{a} & \verb'\ddot{a}' \\
\end{symbols}

\subsection{Size Commands}
\vspace*{-1ex}
\begin{symbols}
\mu~\zsmall\mu~\zSmall\mu &\verb'\mu \zsmall\mu \zSmall\mu'\\
\zbig\mu~\zBig\mu~\zBIG\mu &\verb'\zbig\mu \zBig\mu \zBIG\mu'\\
\end{symbols}
\end{document}
-----------end of oz.tex----------cut here for threecolumn.sty-----
% Document sub-style threecolumn.sty   May 23, 1989
%
% Author: George D. Greenwade, Director, Center for Business and Economic
%  Research, Sam Houston State University, Huntsville, TX 77341-2056
%  Voice: (409) 294-1518    Bitnet: BED_GDG@SHSU.BITNET
%
% Date of Release:  May 23, 1989  (original version)
% Revision History:
%
% Purpose: To create LaTeX output in three columns without corrupting the
%  general uses of LaTeX.  This version is not suggested for use unless the
%  ENTIRE DOCUMENT is to be in a three column output with no multiple column
%  floats.
%
% Usage:  Preamble: \documentstyle[...,threecolumn]{...}
%         In text:  \threecolumn
%
% Features: Addition of \photo{height}{caption} to create an empty box of the
%  dimension \columnwidth wide and specified height (#1), with a caption below
%  set in the \sl font.  Height MUST be specified, caption may be blank, but
%  must be left as a null entry (i.e., \photo{2in}{} for a 2-inch blank space).
%  \photo is placed on a minipage within a table[ht].  The caption is photo-
%  specific and does not step the table counter (as best as I can tell).
%
% Known Limitations (which would be nice ot fix):  May 23, 1989
%  (1) \threecolumn does NOT presently handle MULTIPLE COLUMN table and figure
%      floats properly, but does properly handle footnotes; however, there are
%      no apparent float handling problem in \twocolumn or \onecolumn.
%  (2) Switching from \onecolumn to \twocolumn and \onecolumn to \threecolumn
%      behave properly.  Switching from \threecolumn to \twocolumn,
%      \threecolumn to \onecolumn, \twocolumn to \theeecolumn, and \twocolumn
%      to \onecolumn generates a blank (but numbered) page.  As a rule,
%      \twocolumn presents strange output results in this sub-style.
%  (3) \maketitle is inoperable in \threecolumn.
%
% Copyright (c) 1989 by George D. Greenwade
% Permission to copy all or part of this work is granted, provided that the
% copies are not made or distributed for resale, and that the copyright notice
% and this notice are retained.
%
% THIS WORK IS PROVIDED ON AN "AS IS" BASIS.  THE AUTHOR PROVIDES NO WARRANTY
% WHATSOEVER, EITHER EXPRESS OR IMPLIED, REGARDING THE WORK, INCLUDING
% WARRANTIES WITH RESPECT TO ITS MERCHANTABILITY OR FITNESS FOR ANY PARTICULAR
% PURPOSE.
%
% Please forward all fixes and improvements which do not otherwise corrupt the
% operation of the LaTeX document processing program to the author.
\typeout{Document Style Option 'threecolumn'.  Released 23 May 1989}

\hoffset -.4in                  % Generalized page layout for three column
\voffset -.3in                  %  output.  Certainly, these are subject to
\columnsep 15pt                 %  customization, but these definitions seem to
\textwidth 7.2in                %  provide efficient default margins.
\textheight 9.5in               %
\topmargin 0pt                  %
\headsep 0pt                    %
\headheight 0pt                 %
\oddsidemargin 0pt              %
\pretolerance=500               % Needed pretolerance and tolerance to assure
\tolerance=10000                %  text generally fits the columns
\doublehyphendemerits=100000    % Inhibit consecutive line hyphens
\brokenpenalty=10000            % Inhibit broken words across columns/pages
\widowpenalty=10000             % Inhibit widows at bottom of page
\clubpenalty=10000              % Inhibit orphans at top of page

\newif\if@threecolumn   \@threecolumnfalse   % New ifs used in routine
\newif\if@secondcolumn  \@secondcolumnfalse  %
\newif\if@thirdcolumn   \@thirdcolumnfalse   %
\newbox\@centercolumn                        % New box to place center column
\newdimen\photoblock \photoblock=0pt         % New dimension used in \photo

\def\onecolumn{\clearpage             % Redefine \onecolumn without corruption
     \global\columnwidth\textwidth
     \global\hsize\columnwidth \global\linewidth\columnwidth
     \global\@twocolumnfalse \global\@threecolumnfalse
     \global\@secondcolumnfalse \global\@thirdcolumnfalse
     \@floatplacement}

\def\twocolumn{\clearpage             % Redefine \twocolumn without corruption
     \global\columnwidth\textwidth
     \global\advance\columnwidth -\columnsep \global\divide\columnwidth\tw@
     \global\hsize\columnwidth \global\linewidth\columnwidth
     \global\@twocolumntrue \global\@threecolumnfalse
     \global\@firstcolumntrue \global\@secondcolumnfalse
     \global\@thirdcolumnfalse
     \@dblfloatplacement\@ifnextchar[{\@topnewpage}{}}

\def\threecolumn{\clearpage             % Define \threeecolumn (very rough;
     \global\columnwidth\textwidth      %   handles floats poorly, if at all)
     \global\advance\columnwidth -\columnsep
     \global\advance\columnwidth -\columnsep \global\divide\columnwidth\thr@@
     \global\hsize\columnwidth \global\linewidth\columnwidth
     \global\@twocolumnfalse \global\@threecolumntrue \global\@firstcolumntrue
     \global\@secondcolumnfalse \global\@thirdcolumnfalse
     \@dblfloatplacement\@ifnextchar[{\@topnewpage}{}}

\def\@doclearpagethree{\ifvoid\footins  % Define variation of \@doclearpage
        \setbox\@tempboxa\vsplit\@cclv to\z@ \unvbox\@tempboxa
%WAS        \setbox\@tempboxa\box\@ccl
        \setbox\@tempboxa\box\@cclv
        \xdef\@deferlist{\@toplist\@botlist
            \@deferlist}\gdef\@toplist{}\gdef\@botlist{}\global\@colroom\@colht
             \ifx\@currlist
              \@empty\else\@latexerr{Float(s)
                 lost}\@ehb\gdef\@currlist{}\fi
       \@makefcolumn\@deferlist
        \@whilesw\if@fcolmade \fi{\@opcol
                                  \@makefcolumn\@deferlist}\if@threecolumn
           \if@firstcolumn
             \xdef\@dbldeferlist{\@dbltoplist
                 \@dbldeferlist}\gdef\@dbltoplist{}\global\@colht\textheight
              \begingroup \@dblfloatplacement \@makefcolumn\@dbldeferlist
               \@whilesw\if@fcolmade \fi \endgroup
           \if@secondcolumn
             {\@outputpage\@makefcolumn\@dbldeferlist} \fi \endgroup
           \else \vbox{}\clearpage
        \fi\fi
     \else\setbox\@cclv\vbox{\box\@cclv\vfil}\@makecol\@opcol
      \clearpage
     \fi}

\def\@specialoutput{\ifnum\outputpenalty > -\@Mii  % Redefine \@specialoutput
    \if@threecolumn \@doclearpagethree             %  to handle \threecolumn
    \else \@doclearpage \fi                        %  environment.
  \else
    \ifnum \outputpenalty <-\@Miii
       \ifnum\outputpenalty<-\@MM \deadcycles\z@\fi
       \global\setbox\@holdpg\vbox{\unvbox\@cclv}
%WAS:    \else \setbox\@tempboxa\box\@ccl
    \else \setbox\@tempboxa\box\@cclv
        \@pagedp\dp\@holdpg \@pageht\ht\@holdpg
        \unvbox\@holdpg
        \ifvoid\footins\else\advance\@pageht\ht\footins
          \advance\@pageht\skip\footins \advance\@pagedp\dp\footins
          \insert\footins{\unvbox\footins}\fi
        \@next\@currbox\@currlist{\ifnum\count\@currbox >\z@
            \@addtocurcol\else\@addmarginpar\fi}\@latexbug
    \ifnum \outputpenalty <\z@ \penalty \z@ \fi
  \fi\fi}

\def\@opcol{\global\@mparbottom\z@   % Redefine \@opcol to handle \threecolumn
    \if@twocolumn\@outputdblcol \fi  %   environment without corruption
    \if@threecolumn\@outputtplcol\else
    \@outputpage \global\@colht\textheight \fi}

\def\@skipcolumn{\if@firstcolumn  % Tentatively define \@skipcolumn (for future
  \global\@firstcolumnfalse       %  use in two-column-wide material in the
  \global\@secondcolumnfalse      %  \threecolumn environment)  NOT EMPLOYED!
  \global\@thirdcolumntrue \fi
  \if@secondcolumn \global\@firstcolumntrue \global\@secondcolumnfalse
  \global\@thirdcolumnfalse \fi}

\def\@outputtplcol{\if@firstcolumn     % Define \@outputtplcol (analogous to
    \global\@firstcolumnfalse          %  \@outputdblcol, but for \threecolumn)
    \global\@secondcolumntrue \global\@thirdcolumnfalse
    \global\setbox\@leftcolumn\box\@outputbox
\else
  \if@secondcolumn \global\@secondcolumnfalse \global\@thirdcolumntrue
   \global\setbox\@centercolumn\box\@outputbox
\else
\global\@thirdcolumnfalse \global\@firstcolumntrue
    \setbox\@outputbox\vbox{\hbox to\textwidth{\hbox to\columnwidth
      {\box\@leftcolumn \hss}\hfil \vrule width\columnseprule\hfil
\hbox to\columnwidth
      {\hss \box\@centercolumn \hss}\hfil \vrule width\columnseprule\hfil
       \hbox to\columnwidth{\box\@outputbox \hss}}}\@combinedblfloats
       \@outputpage \begingroup \@dblfloatplacement \@startdblcolumn
       \@whilesw\if@fcolmade \fi{\@outputpage\@startdblcolumn}\endgroup
    \fi \fi}

\def\photoblocksize{\global\photoblock=\columnwidth   % Define width of the
   \advance \photoblock -\columnsep                   %  photo block
   \if@threecolumn \advance \photoblock -\columnsep \fi}

\def\photo#1#2{\photoblocksize   % Define \photo{height}{caption} as floating
 \begin{table}[ht]               %  blank space for photo insertions to be used
\begin{minipage}{\photoblock}    %  in final paste-up.
\rule{0pt}{#1}   \\              % #1 is height
\end{minipage}                   % width defaults to column width
\begin{center} {\sl \ #2}        % #2 is caption set in the \sl font face
\end{center}
\end{table}}
-----------------------end of threecolumn.sty-----------------------
--
Paul King							       _--_|\
Dept. of Computer Science, Univ. of Queensland			      /      X
Queensland, Australia, 4072					      \_.--._/
king@batserver.cs.uq.oz.au (ACSNET)				            v