summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/objectz/oz.dtx
diff options
context:
space:
mode:
Diffstat (limited to 'macros/latex/contrib/objectz/oz.dtx')
-rw-r--r--macros/latex/contrib/objectz/oz.dtx1613
1 files changed, 1613 insertions, 0 deletions
diff --git a/macros/latex/contrib/objectz/oz.dtx b/macros/latex/contrib/objectz/oz.dtx
new file mode 100644
index 0000000000..e272cf1572
--- /dev/null
+++ b/macros/latex/contrib/objectz/oz.dtx
@@ -0,0 +1,1613 @@
+\def\fileversion{2.46}
+\def\filedate{1999/05/24}
+\def\docdate {1994/08/13}
+%
+% \iffalse
+%% File: oz.dtx Copyright (C) 1995-1999 Sebastian Rahtz
+% Permission is hereby granted, free of charge, to any person obtaining
+% a copy of this software and associated documentation files (the
+% ``Software''), to deal in the Software without restriction, including
+% without limitation the rights to use, copy, modify, merge, publish,
+% distribute, sublicense, and/or sell copies of the Software, and to
+% permit persons to whom the Software is furnished to do so, subject to
+% the following conditions:
+%
+% The above copyright notice and this permission notice shall be included
+% in all copies or substantial portions of the Software.
+%
+% THE SOFTWARE IS PROVIDED ``AS IS'', WITHOUT WARRANTY OF ANY KIND, EXPRESS
+% OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+% MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+% IN NO EVENT SHALL SEBASTIAN RAHTZ BE LIABLE FOR ANY CLAIM, DAMAGES OR
+% OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
+% ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
+% OTHER DEALINGS IN THE SOFTWARE.
+%
+%<*driver>
+\documentclass{ltxdoc}
+\begin{document}
+ \title{The \textsf{oz} package\thanks{This file
+ has version number \fileversion, last
+ revised \filedate.}}
+ \author{edited by Sebastian Rahtz\\S.Rahtz@elsevier.co.uk}
+ \date{\filedate}
+ \maketitle
+ \tableofcontents
+ \DocInput{oz.dtx}
+\end{document}
+%</driver>
+% \fi
+% \CheckSum{3387}
+%
+% \section{Introduction}
+%
+% This file provides macros to typeset Object Z schemas.
+%\subsection{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:
+% \texttt{mike@prg.oxford.ac.uk}
+%
+% \begin{quote}
+% \begin{tabular}{lp{.6\textwidth}}
+% 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| \& |\def|s 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\\
+% 2 Aug 90 &added |\subseq|, |\iseq| - PK\\
+% \end{tabular}
+%
+% \begin{tabular}{lp{.6\textwidth}}
+% 9 Nov 90 &changed |\M| to hopefully interact better with spacing ---
+% PK\\
+% 18 Dec 90 &changed to new AMS 2.0 fonts - PK (with help from Adrian Lee)\\
+% 11 Feb 91 &added |\poly| |\widen| and modified |\gendef| - PK\\
+% 10 Apr 91 &added |\fuzzcompatible| - PK\\
+% 1 Apr 91 &added |\gengendef| - Steve Atkinson\\
+% 24 Feb 92 &changed to work with NFSS --- Sebastian Rahtz\\
+% 29 Dec 92 &changed to work with NFSS2 --- Sebastian Rahtz\\
+% 23 Dec 93 &checked for |\LaTeXe|\\
+% 6 Jan 94 &checked again for |\LaTeXe| with help of David Carlisle\\
+% 7 Apr 94 & checked again, bundle files added\\
+% 13 Aug 94 & removed hard-wired number of family for math letters\\
+% & removed definition of |\c| as it prevents cedilla from working\\
+% 22 Feb 95 & updated for AMSLaTeX 2.1 and Lucida compatibility\\
+% 30 Aug 96 &added Object-Z notations in Section 2A - SA\\
+% 17 Sep 97 &re-added |\zedbaselinestretch| -- David Leadbetter\\
+% 20 July 98 &|state| environment can be used in |sidebyside| \\
+% &changed to work with |slides| class -- DL\\
+% 4 Nov 98 & fixed |\zedbaselinestretch| -- DL\\
+% 17 Nov 98 & fixed |\Init|, etc -- DL\\
+% 24 May 99 & removed extra space output by |\fontsize| -- Ian Hayes and DL
+% \end{tabular}
+% \end{quote}
+%
+%\subsection{Known Problems}
+%
+%\begin{enumerate}
+% \item |\bBigg| defines |\zBig|, etc as fixed font sizes -
+% in the original oz.sty (for \LaTeX 2.09) these sizing commands change
+% the font size relative to the current font size (so a |\zBig|
+% in the scope of a |\large| is bigger than a |\zBig|
+% in the scope of a |\normalsize|);
+% \item |sidebyside| works very poorly with the |class| environment
+% - indentation of operation schemas is wrong;
+% \item the |calc| package is needed for |\zedbaselinestretch|.
+%\end{enumerate}
+%
+%
+%\subsection{The Object-Z Homepage}
+%
+% The Object-Z homepage (http://svrc.it.uq.edu.au/Object-Z/) contains:
+%
+% \begin{itemize}
+% \item Papers and Tech-reports on Object-Z;
+% \item {\bf wizard} - the Object-Z type checker.
+% \end{itemize}
+%
+% \noindent Please post any updates that you may make to this file to the
+% Formal Methods Group -- fmg@it.uq.edu.au
+%
+%
+%
+% \newpage
+%
+% \StopEventually{}
+%
+% \begin{macrocode}
+%<*package>
+\NeedsTeXFormat{LaTeX2e}[1994/12/01]
+\ProvidesPackage{oz}[\filedate\space\fileversion\space Object Z macros]
+\message{`Object-Z Macros' \fileversion\space <\filedate>}
+\RequirePackage{calc}
+% \end{macrocode}
+% The \LaTeXe\ parbox code is much more complicated, so we get back
+% a simpler world from \LaTeX 209.
+% \begin{macrocode}
+\def\oz@parbox{\@ifnextchar [{\oz@iparbox}{\oz@iparbox[c]}}
+\long\def\oz@iparbox[#1]#2#3{\leavevmode \@pboxswfalse
+ \if #1b\vbox
+ \else \if #1t\vtop
+ \else \vbox
+ %\ifmmode \vcenter \else \@pboxswtrue $\vcenter \fi
+ \fi
+ \fi
+{\hsize #2\@parboxrestore #3}
+ %\if@pboxsw \m@th$\fi
+}
+% \end{macrocode}
+%
+%\section{Z fonts}
+%
+% The AMS extra symbol fonts are loaded if we are not using Lucida New Math.
+% Note: msam and msbm 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)
+%
+% \begin{macrocode}
+\@ifpackageloaded{lucbr}{}{%
+\DeclareMathVersion{oz}
+\SetMathAlphabet{\mathrm}{oz}{\encodingdefault}{\rmdefault}{m}{n}%
+\SetMathAlphabet{\mathbf}{oz}{\encodingdefault}{\rmdefault}{bx}{n}%
+\SetMathAlphabet{\mathsf}{oz}{\encodingdefault}{\sfdefault}{m}{n}%
+\DeclareSymbolFont{italics}{\encodingdefault}{\rmdefault}{m}{it}%
+\DeclareSymbolFontAlphabet{\mathrm}{operators}
+\DeclareSymbolFontAlphabet{\mathit}{letters}
+\DeclareSymbolFontAlphabet{\mathcal}{symbols}
+\DeclareSymbolFontAlphabet{\ozit}{italics}
+\DeclareSymbolFont{lasy}{U}{lasy}{m}{n}
+\DeclareSymbolFont{AMSa}{U}{msa}{m}{n}
+\DeclareSymbolFont{AMSb}{U}{msb}{m}{n}
+\let\mho\undefined
+\let\Join\undefined
+\let\Box\undefined
+\let\Diamond\undefined
+\let\leadsto\undefined
+\let\sqsubset\undefined
+\let\sqsupset\undefined
+\let\lhd\undefined
+\let\unlhd\undefined
+\let\rhd\undefined
+\let\unrhd\undefined
+\DeclareMathSymbol{\mho}{\mathord}{lasy}{"30}
+\DeclareMathSymbol{\Join}{\mathrel}{lasy}{"31}
+\DeclareMathSymbol{\Box}{\mathord}{lasy}{"32}
+\DeclareMathSymbol{\Diamond}{\mathord}{lasy}{"33}
+\DeclareMathSymbol{\leadsto}{\mathrel}{lasy}{"3B}
+\DeclareMathSymbol{\sqsubset}{\mathrel}{lasy}{"3C}
+\DeclareMathSymbol{\sqsupset}{\mathrel}{lasy}{"3D}
+\DeclareMathSymbol{\lhd}{\mathrel}{lasy}{"01}
+\DeclareMathSymbol{\unlhd}{\mathrel}{lasy}{"02}
+\DeclareMathSymbol{\rhd}{\mathrel}{lasy}{"03}
+\DeclareMathSymbol{\unrhd}{\mathrel}{lasy}{"04}
+\DeclareSymbolFontAlphabet{\mathbb}{AMSb}
+\DeclareSymbolFontAlphabet{\bbold}{AMSb}
+\mathversion{oz}
+}
+% \end{macrocode}
+%
+% Allow change of size within schemas. This is a sod to get right;
+% my principle (eventually!) was to go out of math temporarily, change
+% size, go into an inner math, do the business, then get out of math
+% and back to outer math.
+%
+% \begin{macrocode}
+\newbox\strutbox@
+\def\strut@{\copy\strutbox@}
+\addto@hook\every@math@size{%
+ \setbox\strutbox@\hbox{\lower.5\normallineskiplimit
+ \vbox{\kern-\normallineskiplimit\copy\strutbox}}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% NOTE: bBigg is used to define the font size for zbig etc
+%% however it defines these as fixed sizes.
+%% The 209 definitions set the font size dependent on the
+%% current point size.
+%%
+%% Hence in 209 you can do \Large\cnj and the symbol is bigger
+%% But in 2e it remains a fixed size!
+%%
+%% This is a problem for the Object-Z operators as originally
+%% defined in the 209 oz.sty `96 file.
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\def\bBigg@#1#2{%
+\mbox{\ifcase#1\or\large\or\Large\or\LARGE\or\small\or\footnotesize\fi
+$#2$}\nulldelimiterspace\z@ \m@th}
+\addto@hook\every@math@size{\setbox\z@\vbox{\hbox{$($}\kern\z@}%
+ \big@size 1.2\ht\z@}
+\newdimen\big@size
+\def\zBIG{\bBigg@{3}}
+\def\zBig{\bBigg@{2}}
+\def\zbig{\bBigg@{1}}
+\def\zsmall{\bBigg@{4}}
+\def\zSmall{\bBigg@{5}}
+% \end{macrocode}
+%
+% WORD STYLES
+% these need handling a bit differently in NFSS from the original.
+%
+% \begin{macrocode}
+\def\String#1{\hbox{`\texttt{#1}'}}
+\def\STRING#1{\hbox{``\texttt{#1}''}}
+\def\infix#1{\z@rel{{\underline{#1}}}}
+\def\word#1{\z@op{#1}}
+\def\keyword#1{\z@op{\mbox{\textrm{#1}}}}
+\def\boldword#1{\z@op{\mbox{\textbf{#1}}}}
+\def\underword#1{\z@op{{\underline{#1}}}}
+\def\underkeyword#1{\z@op{{\underline{\mbox{\textrm{#1}}}}}}
+\def\underboldword#1{\z@op{{\underline{\mbox{\textbf{#1}}}}}}
+% \end{macrocode}
+%
+%\section{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|.
+%
+% \begin{macrocode}
+\def\@setmcodes#1#2#3{{\count0=#1 \count1=#3
+ \loop \global\mathcode\count0=\count1 \ifnum \count0<#2
+ \advance\count0 by1 \advance\count1 by1 \repeat}}
+% \end{macrocode}
+% Use |\hexnumber@\symitalics|
+% in case other families are loaded before.
+% (from D. Roegel, July 13, 1994)
+% \begin{macrocode}
+\@setmcodes{`A}{`Z}{"7\hexnumber@\symitalics41}
+\@setmcodes{`a}{`z}{"7\hexnumber@\symitalics61}
+% \end{macrocode}
+%
+% 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.
+%
+% \begin{macrocode}
+\let\@mc=\mathchardef
+\mathcode`\;="8000 % Makes ; active in math mode
+{\catcode`\;=\active \gdef;{\semicolon\;}}
+\@mc\semicolon="603B
+% \end{macrocode}
+%
+%\section{Utility macros for Z symbols}
+%\begin{tabular}{ll}
+% |\z@op |& makes a large math operator\\
+% |\z@rel|& makes a math relation\\
+% |\z@bin|& makes a binary operator\\
+%\end{tabular}
+%
+% Each use a mathstrut to defeat TeX's vertical adjustment.
+% |\z@bigXXX| is a big version of symbol
+%
+% \begin{macrocode}
+\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}}}
+% \end{macrocode}
+%
+% This underscore doesn't have the little kern --- you get an italic
+% correction anyway in math mode.
+% \begin{macrocode}
+\def\_{\leavevmode \vbox{\hrule width0.4em}}
+% \end{macrocode}
+% Save |\q| as |\xq| for quantifiers q.
+% \begin{macrocode}
+\let\xforall=\forall
+\let\xexists=\exists
+\let\xlambda=\lambda
+\let\xmu=\mu
+% \end{macrocode}
+% Save other symbols
+% \begin{macrocode}
+\let\xsucc\succ
+\let\xprec\prec
+\let\dotaccent=\dot
+\let\sectionsymbol=\S
+\let\integral=\int
+\let\product\prod
+% \end{macrocode}
+% |\p| and |\f| make arrows with 1 and 2 crossings resp.
+% \begin{macrocode}
+\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$}}}
+\@ifpackageloaded{lucbr}{%
+ \DeclareMathSymbol{\doublebarwedge}{\mathbin}{symbols}{"D4}
+ \DeclareMathSymbol{\lll}{\mathrel}{letters}{"DE}
+ \DeclareMathSymbol{\ggg}{\mathrel}{letters}{"DF}
+ \DeclareMathSymbol{\eth}{\mathrel}{operators}{"F0}
+}{%
+% \end{macrocode}
+%\section{Amstex symbol definitions}
+%
+% Do these before Z symbols so that we can use them in our special symbols.
+% AMSa font:
+% \begin{macrocode}
+\let\rightleftharpoons\undefined
+\let\angle\undefined
+\DeclareMathSymbol\boxdot{\mathbin}{AMSa}{"00}
+\DeclareMathSymbol\boxplus{\mathbin}{AMSa}{"01}
+\DeclareMathSymbol\boxtimes{\mathbin}{AMSa}{"02}
+\DeclareMathSymbol\square{\mathord}{AMSa}{"03}
+\DeclareMathSymbol\blacksquare{\mathord}{AMSa}{"04}
+\DeclareMathSymbol\centerdot{\mathbin}{AMSa}{"05}
+\DeclareMathSymbol\lozenge{\mathord}{AMSa}{"06}
+\DeclareMathSymbol\blacklozenge{\mathord}{AMSa}{"07}
+\DeclareMathSymbol\circlearrowright{\mathrel}{AMSa}{"08}
+\DeclareMathSymbol\circlearrowleft{\mathrel}{AMSa}{"09}
+\DeclareMathSymbol\rightleftharpoons{\mathrel}{AMSa}{"0A}
+\DeclareMathSymbol\leftrightharpoons{\mathrel}{AMSa}{"0B}
+\DeclareMathSymbol\boxminus{\mathbin}{AMSa}{"0C}
+\DeclareMathSymbol\Vdash{\mathrel}{AMSa}{"0D}
+\DeclareMathSymbol\Vvdash{\mathrel}{AMSa}{"0E}
+\DeclareMathSymbol\vDash{\mathrel}{AMSa}{"0F}
+\DeclareMathSymbol\twoheadrightarrow{\mathrel}{AMSa}{"10}
+\DeclareMathSymbol\twoheadleftarrow{\mathrel}{AMSa}{"11}
+\DeclareMathSymbol\leftleftarrows{\mathrel}{AMSa}{"12}
+\DeclareMathSymbol\rightrightarrows{\mathrel}{AMSa}{"13}
+\DeclareMathSymbol\upuparrows{\mathrel}{AMSa}{"14}
+\DeclareMathSymbol\downdownarrows{\mathrel}{AMSa}{"15}
+\DeclareMathSymbol\upharpoonright{\mathrel}{AMSa}{"16}
+\DeclareMathSymbol\downharpoonright{\mathrel}{AMSa}{"17}
+\DeclareMathSymbol\upharpoonleft{\mathrel}{AMSa}{"18}
+\DeclareMathSymbol\downharpoonleft{\mathrel}{AMSa}{"19}
+\DeclareMathSymbol\rightarrowtail{\mathrel}{AMSa}{"1A}
+\DeclareMathSymbol\leftarrowtail{\mathrel}{AMSa}{"1B}
+\DeclareMathSymbol\leftrightarrows{\mathrel}{AMSa}{"1C}
+\DeclareMathSymbol\rightleftarrows{\mathrel}{AMSa}{"1D}
+\DeclareMathSymbol\Lsh{\mathrel}{AMSa}{"1E}
+\DeclareMathSymbol\Rsh{\mathrel}{AMSa}{"1F}
+\DeclareMathSymbol\rightsquigarrow{\mathrel}{AMSa}{"20}
+\DeclareMathSymbol\leftrightsquigarrow{\mathrel}{AMSa}{"21}
+\DeclareMathSymbol\looparrowleft{\mathrel}{AMSa}{"22}
+\DeclareMathSymbol\looparrowright{\mathrel}{AMSa}{"23}
+\DeclareMathSymbol\circeq{\mathrel}{AMSa}{"24}
+\DeclareMathSymbol\succsim{\mathrel}{AMSa}{"25}
+\DeclareMathSymbol\gtrsim{\mathrel}{AMSa}{"26}
+\DeclareMathSymbol\gtrapprox{\mathrel}{AMSa}{"27}
+\DeclareMathSymbol\multimap{\mathrel}{AMSa}{"28}
+\DeclareMathSymbol\therefore{\mathrel}{AMSa}{"29}
+\DeclareMathSymbol\because{\mathrel}{AMSa}{"2A}
+\DeclareMathSymbol\doteqdot{\mathrel}{AMSa}{"2B}
+\DeclareMathSymbol\triangleq{\mathrel}{AMSa}{"2C}
+\DeclareMathSymbol\precsim{\mathrel}{AMSa}{"2D}
+\DeclareMathSymbol\lesssim{\mathrel}{AMSa}{"2E}
+\DeclareMathSymbol\lessapprox{\mathrel}{AMSa}{"2F}
+\DeclareMathSymbol\eqslantless{\mathrel}{AMSa}{"30}
+\DeclareMathSymbol\eqslantgtr{\mathrel}{AMSa}{"31}
+\DeclareMathSymbol\curlyeqprec{\mathrel}{AMSa}{"32}
+\DeclareMathSymbol\curlyeqsucc{\mathrel}{AMSa}{"33}
+\DeclareMathSymbol\preccurlyeq{\mathrel}{AMSa}{"34}
+\DeclareMathSymbol\leqq{\mathrel}{AMSa}{"35}
+\DeclareMathSymbol\leqslant{\mathrel}{AMSa}{"36}
+\DeclareMathSymbol\lessgtr{\mathrel}{AMSa}{"37}
+\DeclareMathSymbol\backprime{\mathord}{AMSa}{"38}
+\DeclareMathSymbol\risingdotseq{\mathrel}{AMSa}{"3A}
+\DeclareMathSymbol\fallingdotseq{\mathrel}{AMSa}{"3B}
+\DeclareMathSymbol\succcurlyeq{\mathrel}{AMSa}{"3C}
+\DeclareMathSymbol\geqq{\mathrel}{AMSa}{"3D}
+\DeclareMathSymbol\geqslant{\mathrel}{AMSa}{"3E}
+\DeclareMathSymbol\gtrless{\mathrel}{AMSa}{"3F}
+\DeclareMathSymbol\sqsubset{\mathrel}{AMSa}{"40}
+\DeclareMathSymbol\sqsupset{\mathrel}{AMSa}{"41}
+\DeclareMathSymbol\vartriangleright{\mathrel}{AMSa}{"42}
+\DeclareMathSymbol\vartriangleleft{\mathrel}{AMSa}{"43}
+\DeclareMathSymbol\trianglerighteq{\mathrel}{AMSa}{"44}
+\DeclareMathSymbol\trianglelefteq{\mathrel}{AMSa}{"45}
+\DeclareMathSymbol\bigstar{\mathord}{AMSa}{"46}
+\DeclareMathSymbol\between{\mathrel}{AMSa}{"47}
+\DeclareMathSymbol\blacktriangledown{\mathord}{AMSa}{"48}
+\DeclareMathSymbol\blacktriangleright{\mathrel}{AMSa}{"49}
+\DeclareMathSymbol\blacktriangleleft{\mathrel}{AMSa}{"4A}
+\DeclareMathSymbol\vartriangle{\mathord}{AMSa}{"4D}
+\DeclareMathSymbol\blacktriangle{\mathord}{AMSa}{"4E}
+\DeclareMathSymbol\triangledown{\mathord}{AMSa}{"4F}
+\DeclareMathSymbol\eqcirc{\mathrel}{AMSa}{"50}
+\DeclareMathSymbol\lesseqgtr{\mathrel}{AMSa}{"51}
+\DeclareMathSymbol\gtreqless{\mathrel}{AMSa}{"52}
+\DeclareMathSymbol\lesseqqgtr{\mathrel}{AMSa}{"53}
+\DeclareMathSymbol\gtreqqless{\mathrel}{AMSa}{"54}
+\DeclareMathSymbol\Rrightarrow{\mathrel}{AMSa}{"56}
+\DeclareMathSymbol\Lleftarrow{\mathrel}{AMSa}{"57}
+\DeclareMathSymbol\veebar{\mathbin}{AMSa}{"59}
+\DeclareMathSymbol\barwedge{\mathbin}{AMSa}{"5A}
+\DeclareMathSymbol\doublebarwedge{\mathbin}{AMSa}{"5B}
+\DeclareMathSymbol\angle{\mathord}{AMSa}{"5C}
+\DeclareMathSymbol\measuredangle{\mathord}{AMSa}{"5D}
+\DeclareMathSymbol\sphericalangle{\mathord}{AMSa}{"5E}
+\DeclareMathSymbol\varpropto{\mathrel}{AMSa}{"5F}
+\DeclareMathSymbol\smallsmile{\mathrel}{AMSa}{"60}
+\DeclareMathSymbol\smallfrown{\mathrel}{AMSa}{"61}
+\DeclareMathSymbol\Subset{\mathrel}{AMSa}{"62}
+\DeclareMathSymbol\Supset{\mathrel}{AMSa}{"63}
+\DeclareMathSymbol\Cup{\mathbin}{AMSa}{"64}
+\DeclareMathSymbol\Cap{\mathbin}{AMSa}{"65}
+\DeclareMathSymbol\curlywedge{\mathbin}{AMSa}{"66}
+\DeclareMathSymbol\curlyvee{\mathbin}{AMSa}{"67}
+\DeclareMathSymbol\leftthreetimes{\mathbin}{AMSa}{"68}
+\DeclareMathSymbol\rightthreetimes{\mathbin}{AMSa}{"69}
+\DeclareMathSymbol\subseteqq{\mathrel}{AMSa}{"6A}
+\DeclareMathSymbol\supseteqq{\mathrel}{AMSa}{"6B}
+\DeclareMathSymbol\bumpeq{\mathrel}{AMSa}{"6C}
+\DeclareMathSymbol\Bumpeq{\mathrel}{AMSa}{"6D}
+\DeclareMathSymbol\lll{\mathrel}{AMSa}{"6E}
+\DeclareMathSymbol\ggg{\mathrel}{AMSa}{"6F}
+\DeclareMathDelimiter\ulcorner{4}{AMSa}{"70}{AMSa}{"70}
+\DeclareMathDelimiter\urcorner{5}{AMSa}{"71}{AMSa}{"71}
+\DeclareMathDelimiter\llcorner{4}{AMSa}{"78}{AMSa}{"78}
+\DeclareMathDelimiter\lrcorner{5}{AMSa}{"79}{AMSa}{"79}
+\xdef\yen {\noexpand\mathhexbox\hexnumber@\symAMSa 55 }
+\xdef\checkmark{\noexpand\mathhexbox\hexnumber@\symAMSa 58 }
+\xdef\circledR {\noexpand\mathhexbox\hexnumber@\symAMSa 72 }
+\xdef\maltese {\noexpand\mathhexbox\hexnumber@\symAMSa 7A }
+\DeclareMathSymbol\circledS{\mathord}{AMSa}{"73}
+\DeclareMathSymbol\pitchfork{\mathrel}{AMSa}{"74}
+\DeclareMathSymbol\dotplus{\mathbin}{AMSa}{"75}
+\DeclareMathSymbol\backsim{\mathrel}{AMSa}{"76}
+\DeclareMathSymbol\backsimeq{\mathrel}{AMSa}{"77}
+\DeclareMathSymbol\complement{\mathord}{AMSa}{"7B}
+\DeclareMathSymbol\intercal{\mathbin}{AMSa}{"7C}
+\DeclareMathSymbol\circledcirc{\mathbin}{AMSa}{"7D}
+\DeclareMathSymbol\circledast{\mathbin}{AMSa}{"7E}
+\DeclareMathSymbol\circleddash{\mathbin}{AMSa}{"7F}
+% \end{macrocode}
+%
+%AMSb font:
+%
+% \begin{macrocode}
+\DeclareMathSymbol\lvertneqq{\mathrel}{AMSb}{"00}
+\DeclareMathSymbol\gvertneqq{\mathrel}{AMSb}{"01}
+\DeclareMathSymbol\nleq{\mathrel}{AMSb}{"02}
+\DeclareMathSymbol\ngeq{\mathrel}{AMSb}{"03}
+\DeclareMathSymbol\nless{\mathrel}{AMSb}{"04}
+\DeclareMathSymbol\ngtr{\mathrel}{AMSb}{"05}
+\DeclareMathSymbol\nprec{\mathrel}{AMSb}{"06}
+\DeclareMathSymbol\nsucc{\mathrel}{AMSb}{"07}
+\DeclareMathSymbol\lneqq{\mathrel}{AMSb}{"08}
+\DeclareMathSymbol\gneqq{\mathrel}{AMSb}{"09}
+\DeclareMathSymbol\nleqslant{\mathrel}{AMSb}{"0A}
+\DeclareMathSymbol\ngeqslant{\mathrel}{AMSb}{"0B}
+\DeclareMathSymbol\lneq{\mathrel}{AMSb}{"0C}
+\DeclareMathSymbol\gneq{\mathrel}{AMSb}{"0D}
+\DeclareMathSymbol\npreceq{\mathrel}{AMSb}{"0E}
+\DeclareMathSymbol\nsucceq{\mathrel}{AMSb}{"0F}
+\DeclareMathSymbol\precnsim{\mathrel}{AMSb}{"10}
+\DeclareMathSymbol\succnsim{\mathrel}{AMSb}{"11}
+\DeclareMathSymbol\lnsim{\mathrel}{AMSb}{"12}
+\DeclareMathSymbol\gnsim{\mathrel}{AMSb}{"13}
+\DeclareMathSymbol\nleqq{\mathrel}{AMSb}{"14}
+\DeclareMathSymbol\ngeqq{\mathrel}{AMSb}{"15}
+\DeclareMathSymbol\precneqq{\mathrel}{AMSb}{"16}
+\DeclareMathSymbol\succneqq{\mathrel}{AMSb}{"17}
+\DeclareMathSymbol\precnapprox{\mathrel}{AMSb}{"18}
+\DeclareMathSymbol\succnapprox{\mathrel}{AMSb}{"19}
+\DeclareMathSymbol\lnapprox{\mathrel}{AMSb}{"1A}
+\DeclareMathSymbol\gnapprox{\mathrel}{AMSb}{"1B}
+\DeclareMathSymbol\nsim{\mathrel}{AMSb}{"1C}
+\DeclareMathSymbol\ncong{\mathrel}{AMSb}{"1D}
+%\DeclareMathSymbol\varsubsetneq{\mathrel}{AMSb}{"20}
+%\DeclareMathSymbol\varsupsetneq{\mathrel}{AMSb}{"21}
+\DeclareMathSymbol\nsubseteqq{\mathrel}{AMSb}{"22}
+\DeclareMathSymbol\nsupseteqq{\mathrel}{AMSb}{"23}
+\DeclareMathSymbol\subsetneqq{\mathrel}{AMSb}{"24}
+\DeclareMathSymbol\supsetneqq{\mathrel}{AMSb}{"25}
+%\DeclareMathSymbol\varsubsetneqq{\mathrel}{AMSb}{"26}
+%\DeclareMathSymbol\varsupsetneqq{\mathrel}{AMSb}{"27}
+\DeclareMathSymbol\subsetneq{\mathrel}{AMSb}{"28}
+\DeclareMathSymbol\supsetneq{\mathrel}{AMSb}{"29}
+\DeclareMathSymbol\nsubseteq{\mathrel}{AMSb}{"2A}
+\DeclareMathSymbol\nsupseteq{\mathrel}{AMSb}{"2B}
+\DeclareMathSymbol\nparallel{\mathrel}{AMSb}{"2C}
+\DeclareMathSymbol\nmid{\mathrel}{AMSb}{"2D}
+\DeclareMathSymbol\nshortmid{\mathrel}{AMSb}{"2E}
+\DeclareMathSymbol\nshortparallel{\mathrel}{AMSb}{"2F}
+\DeclareMathSymbol\nvdash{\mathrel}{AMSb}{"30}
+\DeclareMathSymbol\nVdash{\mathrel}{AMSb}{"31}
+\DeclareMathSymbol\nvDash{\mathrel}{AMSb}{"32}
+\DeclareMathSymbol\nVDash{\mathrel}{AMSb}{"33}
+\DeclareMathSymbol\ntrianglerighteq{\mathrel}{AMSb}{"34}
+\DeclareMathSymbol\ntrianglelefteq{\mathrel}{AMSb}{"35}
+\DeclareMathSymbol\ntriangleleft{\mathrel}{AMSb}{"36}
+\DeclareMathSymbol\ntriangleright{\mathrel}{AMSb}{"37}
+\DeclareMathSymbol\nleftarrow{\mathrel}{AMSb}{"38}
+\DeclareMathSymbol\nrightarrow{\mathrel}{AMSb}{"39}
+\DeclareMathSymbol\nLeftarrow{\mathrel}{AMSb}{"3A}
+\DeclareMathSymbol\nRightarrow{\mathrel}{AMSb}{"3B}
+\DeclareMathSymbol\nLeftrightarrow{\mathrel}{AMSb}{"3C}
+\DeclareMathSymbol\nleftrightarrow{\mathrel}{AMSb}{"3D}
+\DeclareMathSymbol\divideontimes{\mathbin}{AMSb}{"3E}
+\DeclareMathSymbol\varnothing{\mathord}{AMSb}{"3F}
+\DeclareMathSymbol\mho{\mathord}{AMSb}{"66}
+\DeclareMathSymbol\eth{\mathord}{AMSb}{"67}
+\DeclareMathSymbol\eqsim{\mathrel}{AMSb}{"68}
+\DeclareMathSymbol\beth{\mathord}{AMSb}{"69}
+\DeclareMathSymbol\gimel{\mathord}{AMSb}{"6A}
+\DeclareMathSymbol\daleth{\mathord}{AMSb}{"6B}
+\DeclareMathSymbol\lessdot{\mathrel}{AMSb}{"6C}
+\DeclareMathSymbol\gtrdot{\mathrel}{AMSb}{"6D}
+\DeclareMathSymbol\ltimes{\mathbin}{AMSb}{"6E}
+\DeclareMathSymbol\rtimes{\mathbin}{AMSb}{"6F}
+\DeclareMathSymbol\shortmid{\mathrel}{AMSb}{"70}
+\DeclareMathSymbol\shortparallel{\mathrel}{AMSb}{"71}
+\DeclareMathSymbol\smallsetminus{\mathbin}{AMSb}{"72}
+\DeclareMathSymbol\thicksim{\mathrel}{AMSb}{"73}
+\DeclareMathSymbol\thickapprox{\mathrel}{AMSb}{"74}
+\DeclareMathSymbol\approxeq{\mathrel}{AMSb}{"75}
+\DeclareMathSymbol\succapprox{\mathrel}{AMSb}{"76}
+\DeclareMathSymbol\precapprox{\mathrel}{AMSb}{"77}
+\DeclareMathSymbol\curvearrowleft{\mathrel}{AMSb}{"78}
+\DeclareMathSymbol\curvearrowright{\mathrel}{AMSb}{"79}
+\DeclareMathSymbol\digamma{\mathord}{AMSb}{"7A}
+\DeclareMathSymbol\varkappa{\mathord}{AMSb}{"7B}
+\DeclareMathSymbol\hslash{\mathord}{AMSb}{"7D}
+\DeclareMathSymbol\hbar{\mathord}{AMSb}{"7E}
+\DeclareMathSymbol\backepsilon{\mathrel}{AMSb}{"7F}
+}
+\def\interleave{{\parallel\!\!\vert}}
+\def\shortinterleave{\z@rel{\mathord\shortmid\mathord\shortparallel}}
+\def\napprox{\not\approx}
+\let\restriction\upharpoonright
+\let\Doteq\doteqdot
+\let\doublecup\Cup
+\let\llless\lll
+\let\gggtr\ggg
+\let\doublecap\Cap
+% \end{macrocode}
+%
+% Numbers
+%
+% \begin{macrocode}
+\def \nat {{\mathbb N}}
+\def \integer {{\mathbb Z}}
+\def \natone {{\mathbb N}_1}
+\def \real {{\mathbb R}}
+\def \bool {{\mathbb B}}
+\let \divides \div
+\def \div {\z@bin{\mathrm{div}}}
+\def \mod {\z@bin{\mathrm{mod}}}
+\def \succ {\word{succ}}
+\def \expon {^}
+% \end{macrocode}
+% aliases
+% \begin{macrocode}
+\let \num \integer
+\let \nplus \natone
+% \end{macrocode}
+%
+% Logic
+%
+% \begin{macrocode}
+\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}
+\@ifpackageloaded{lucbr}{%
+\DeclareMathSymbol{\nexi}{0}{arrows}{"20}
+}{%
+\DeclareMathSymbol{\nexi}{\mathord}{AMSb}{"40}
+}
+\def \dot {\z@rel{\bullet}}
+\def \true {\keyword{true}}
+\def \false {\keyword{false}}
+\let \cond \rightarrow
+% \end{macrocode}
+% aliases
+% \begin{macrocode}
+\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
+% \end{macrocode}
+%
+% SETS
+%
+% \begin{macrocode}
+\let \emptyset \varnothing
+\def \varemptyset {\{\,\}}
+\def \pset {\z@op{\mathbb P}}
+\def \psetone {\pset_1}
+\def \fset {\z@op{\mathbb F}}
+\def \fsetone {\fset_1}
+\def \sset {\z@op{\mathbb 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}}
+% \end{macrocode}
+% aliases
+% \begin{macrocode}
+\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
+% \end{macrocode}
+%
+% RELATIONS \& FUNCTIONS
+%
+% \begin{macrocode}
+\def \lambda {\z@op{\xlambda}}
+\def \mu {\z@op{\xmu}}
+\def \dom {\keyword{dom}}
+\def \ran {\keyword{ran}}
+\def \id {\keyword{id}}
+\@ifpackageloaded{lucbr}{%
+\DeclareMathSymbol{\dres}{\mathbin}{letters}{"2F}
+\DeclareMathSymbol{\rres}{\mathbin}{letters}{"2E}
+}{%
+\DeclareMathSymbol{\dres}{\mathbin}{AMSa}{"43}
+\DeclareMathSymbol{\rres}{\mathbin}{AMSa}{"42}
+}
+\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
+ \mathrm{o}$\hfil\cr\hfil$\scriptscriptstyle\mathrm{9}$\hfil}}}}
+\def \inv {^\sim}
+\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 {^}
+% \end{macrocode}
+% aliases
+% \begin{macrocode}
+\let \comp \fcmp
+\let \ndres \dsub
+\let \nrres \rsub
+\let \fun \tfun
+\let \inj \tinj
+\let \surj \tsur
+\let \psurj \psur
+\let \llless \lll
+\let \gggtr \ggg
+\def \interleave {{\parallel\!\!\vert}}
+\def \shortinterleave {\z@rel{\mathord\shortmid\mathord\shortparallel}}
+\let \restriction \upharpoonright
+\def \napprox {\not\approx}
+% \end{macrocode}
+%
+% SEQUENCES
+% \begin{macrocode}
+\def \seq {\keyword{seq}}
+\def \iseq {\keyword{iseq}}
+\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}}
+\@ifpackageloaded{lucbr}{%
+\DeclareMathSymbol{\sres}{2}{arrows}{"75}
+\DeclareMathSymbol{\ires}{2}{arrows}{"76}
+\DeclareMathSymbol{\@@cat}{\mathbin}{operators}{"5F}
+}{%
+\DeclareMathSymbol{\@@cat}{\mathbin}{AMSa}{"61}
+\DeclareMathSymbol{\sres}{\mathbin}{AMSa}{"16}
+\DeclareMathSymbol{\ires}{\mathbin}{AMSa}{"18}
+}
+\def \cat {\mathbin{\raise 0.8ex\hbox{$\mathchar\@@cat$}}}
+\def \ssub {\z@bin{\rlap{$-$}{\sres}}}
+\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 \partition {\keyword{partitions}}
+\def \disjoint {\keyword{disjoint}}
+\def \subseq {\keyword{subseq}}
+% \end{macrocode}
+% aliases
+% \begin{macrocode}
+\let \filter \sres
+% \end{macrocode}
+%
+% Schemas:
+%
+% \begin{macrocode}
+\def \lsch {\z@bigop{[}}
+\def \rsch {\z@bigop{]}}
+\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]}
+% \end{macrocode}
+% aliases
+% \begin{macrocode}
+\let \project \zproject
+\let \import \sres
+\let \semi \zcmp
+\let \hide \zhide
+% \end{macrocode}
+%
+% BAGS
+%
+% \begin{macrocode}
+\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}}
+% \end{macrocode}
+%
+% Definitions \& declarations
+%
+% \begin{macrocode}
+\def \ddef {\z@rel{\;::=\;}}
+\def \bbar {\z@bigrel{|}}
+\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}
+% \end{macrocode}
+% aliases
+% \begin{macrocode}
+\let \sdefs \sdef
+\mathcode`\|=\mid
+\let \ldata \lang
+\let \rdata \rang
+% \end{macrocode}
+%
+% MISCELLANEOUS
+%
+% \begin{macrocode}
+\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}}
+% \end{macrocode}
+%
+% QZED SUPPORT
+%
+% \begin{macrocode}
+\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}
+% \end{macrocode}
+%
+% CLASSES
+%
+% \begin{macrocode}
+\def\qua{\mbox{::}}
+\def\redef{\mbox{\textbf{~redef}}}
+\def\Init{I\!{\scriptstyle{NIT}}}
+\def\Exit{E\!{\scriptstyle{XIT}}}
+\def\Internal{I\!{\scriptstyle{NTERNAL}}}
+\def\Aux{A\!{\scriptstyle{UX}}}
+\def\intern{\mbox{\textsf{i}}}
+% \end{macrocode}
+%
+% PROOFS
+%
+% \begin{macrocode}
+\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$}}}
+% \end{macrocode}
+% aliases
+% \begin{macrocode}
+\let\shows\thrm
+% \end{macrocode}
+%
+% OBJECT THEORY
+%
+% \begin{macrocode}
+\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}
+% \end{macrocode}
+% aliases
+% \begin{macrocode}
+\let\inherits\childof
+\let\subclass\childof
+\let\isa\childof
+\let\supclass\parentof
+\let\instantiates\hasa
+\let\islikea\weaksubclass
+\def\poly{\mathord\downarrow}
+\def\widen#1{\z@op{{\overline{#1}}}}
+% \end{macrocode}
+%
+% TEMPORAL LOGIC
+%
+% \begin{macrocode}
+\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$}}
+% \end{macrocode}
+% aliases
+% \begin{macrocode}
+\let\henceforth\always
+% \end{macrocode}
+%
+% ORDERS
+%
+% \begin{macrocode}
+\def \mono {\keyword{monotonic}}
+\def \porder {\keyword{partial\_order}}
+\def \torder {\keyword{total\_order}}
+\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}]}}
+% \end{macrocode}
+%
+%\section{Object-Z Notations}
+%
+% KEYWORDS AND KEYSYMBOLS
+%
+% \begin{macrocode}
+\def \oid {{\bbold O}}
+\def \self {\word{self}}
+\def \contained {\word{contained}}
+\let \classuni \uni
+\def \visibility {\zproject}
+\def \invisibility {{\project\hspace{-0.63 em}\cross}}
+% \end{macrocode}
+%
+% CONTAINMENT AND CONTROL ADORNMENTS
+%
+% \begin{macrocode}
+\def \cid {{\bigcirc\mbox{\scriptsize{\hspace{-0.78em}}\mbox{\tiny{C}}}}}
+\def \sid {{\bigcirc\mbox{\scriptsize{\hspace{-0.74em}}\mbox{\tiny{S}}}}}
+\def \eid {{\bigcirc\mbox{\scriptsize{\hspace{-0.74em}}\mbox{\tiny{E}}}}}
+% \end{macrocode}
+%
+% BINARY COMPOSITION OPERATORS
+%
+% \begin{macrocode}
+\def \pll {~\parallel~}
+\def \plo {~\parallel_{!}~}
+\def \sqc {~\semi~}
+\def \cnj {~\zand~}
+\def \gch {~[\mbox{\hspace{-0.06em}}]~}
+\def \enh {~\dot~}
+% \end{macrocode}
+%
+% DISTRIBUTED COMPOSITION OPERATORS
+%
+% \begin{macrocode}
+% Redefined because of \zbig problem
+% \def \dsqc {\mbox{{\Large $\zcmp~$}}}
+\def \dsqc {\mbox{{\Large $\fcmp~$}}}
+\def \dgch {\mbox{{\Large $[\mbox{\hspace{-0.06em}}]$}}}
+% Redefined because of \zbig problem
+% \def \dcnj {\mbox{{\Large $\zand$}}}
+\def \dcnj {\mbox{{\Large $\land$}}}
+\def \dpll {\mbox{{\Large $\parallel$}}}
+\def \dplo {\mbox{{\Large $\parallel_{!}$}}}
+% \end{macrocode}
+%
+%\section{Z environments}
+%
+%\subsection{Margin stack}
+%
+% Define a stack of dimensions (50 elements)
+% This can probably be made smaller when qzed filters its \TeX\ output better
+% \begin{macrocode}
+\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\@gtempa
+\z@stackmax=\allocationnumber
+\dimen\z@stackmin=0pt
+% \end{macrocode}
+% Define a box to contain the current line
+% \& a variable to contain it's indentation
+% \begin{macrocode}
+\newbox\z@curline
+\newdimen\z@curindent
+\dimen\z@curindent=0pt
+% \end{macrocode}
+% Space between operands of a function application
+% \begin{macrocode}
+\def\z@space{{}\;{}}
+% \end{macrocode}
+% Define a box to contain the current field
+% \begin{macrocode}
+\newbox\z@curfield
+% \end{macrocode}
+% Define a mini-tabbing environment for use inside `zed'
+% \begin{macrocode}
+\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
+% \end{macrocode}
+%
+%\subsection{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.
+%
+%\subsubsection{Format and control macros}
+%
+% \begin{macrocode}
+\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}
+\def\baselinestretch{1}
+% \end{macrocode}
+%
+% Penalties
+%
+% \begin{macrocode}
+\newcount\interzedlinepenalty \interzedlinepenalty=10000 %never break
+\newcount\preboxpenalty \preboxpenalty=0 %break easily
+\newcount\forcepagepenalty \forcepagepenalty=-10000 %always break
+\interdisplaylinepenalty=100 %break sometimes
+% \end{macrocode}
+%
+% Macros for changing the size of schema text
+%
+% \begin{macrocode}
+\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\z@zeroskips{\abovedisplayskip\z@\belowdisplayskip\z@
+ \abovedisplayshortskip\z@\belowdisplayshortskip\z@}
+%
+% Make zedbaselinestretch have an automatic effect
+% adapted from lfonts.tex
+%
+\def\@setfontsize#1#2#3{\@nomath#1%
+ \ifx\protect\@typeset@protect
+ \let\@currsize#1%
+ \fi
+ \fontsize{#2}{#3}\selectfont
+ \setlength{\zedbaselineskip}{\baselineskip/\real{\baselinestretch}}%
+ \zedbaselineskip\zedbaselinestretch\zedbaselineskip
+ \setbox\zstrutbox\hbox{\vrule height.7\zedbaselineskip
+ depth.3\zedbaselineskip width\z@}}
+% \end{macrocode}
+%
+%\subsection{Macros for margins}
+%
+% |\z@narrow|, |\z@wide| --- make the margins narrower, wider
+%
+% \begin{macrocode}
+\def\z@narrow{\advance\linewidth by -\zedindent}
+\def\z@wide{\advance\linewidth by \zedindent}
+% \end{macrocode}
+%
+%\subsection{Macros for drawing boxes}
+%
+% |\z@hrulefill| --- line with correct thickness
+%
+% \begin{macrocode}
+\def\z@hrulefill{\leaders\hrule height\zedlinethickness\hfill}
+% \end{macrocode}
+%
+% |\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
+%
+% \begin{macrocode}
+\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
+% \end{macrocode}
+%
+% |\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.
+%
+% \begin{macrocode}
+\def\z@left{\ifz@inbox\vrule width\zedlinethickness\hskip\zedleftsep\fi}
+% \end{macrocode}
+%
+% \subsection{Macros for setting up Z environments}
+%
+% \begin{macrocode}
+\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
+}
+% \end{macrocode}
+%
+% Z lines are formated in two (overlapping) 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.
+%
+% \begin{macrocode}
+\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}
+% \end{macrocode}
+%
+%\subsection{Spacing commands}
+%
+% no vertical glue between abutted lines
+%
+% \begin{macrocode}
+\def\@but{\noalign{\nointerlineskip}}
+% \end{macrocode}
+%
+% 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{}}}|
+% \begin{macrocode}
+\def\z@nopar{\global\@endpetrue}
+% \end{macrocode}
+%
+% |\z@leavevmode| -- Enter horizontal mode, taking account of possible
+% interaction with lists and section heads:
+%\begin{enumerate}
+% \item After a |\item|, use |\indent| to get the label (this
+% fails to run in even short labels).
+% \item After a run-in heading, use |\indent|.
+% \item After an ordinary heading, throw away the |\everypar|
+% tokens, reset |\@nobreak|, and use |\noindent| with |\parskip|
+% zero.
+% \item Otherwise, use |\noindent| with |\parskip| zero
+%\end{enumerate}
+% Use when entering displayed environments to get correct spacing
+%
+% \begin{macrocode}
+\def\z@leavevmode{\ifvmode\if@inlabel\indent\else\if@noskipsec\indent\else
+ \if@nobreak\global\@nobreakfalse\everypar={}\fi
+ {\parskip=0pt\noindent}\fi\fi\fi}
+% \end{macrocode}
+%
+% extra vertical space in non-box environments
+%
+% \begin{macrocode}
+\def\also{\crcr\noalign{\vskip\jot}}
+\def\Also{\crcr\noalign{\vskip2\jot}}
+\def\ALSO{\Also\Also}
+% \end{macrocode}
+%
+% extra vertical space in boxed environments
+%
+% \begin{macrocode}
+\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}
+% \end{macrocode}
+%
+%\subsection{Environment-breaking commands}
+%
+% \begin{macrocode}
+\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}
+% \end{macrocode}
+%
+%\section{Utility macros for Object-Z}
+%
+% \begin{macrocode}
+\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
+ \oz@parbox{\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}
+% \end{macrocode}
+%
+%\section{Non-box environments}
+%
+%
+% ZED for non-box multiline formulas
+%
+% \begin{macrocode}
+\def\zed{\z@outnonbox\z@inboxfalse\z@format}
+\def\endzed{\crcr\egroup\endz@env}
+\let\[=\zed
+\def\]{\crcr\egroup$$\ignorespaces}
+% \end{macrocode}
+%
+% 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.
+%
+% \begin{macrocode}
+\def\argue{\z@outnonbox\interzedlinepenalty=\interdisplaylinepenalty
+ \openup 1\jot \z@format
+ \noalign{\vskip-\jot}}% equal vspace above and below argue display
+\let\endargue=\endzed
+% \end{macrocode}
+%
+% 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.
+%
+% \begin{macrocode}
+\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}
+% \end{macrocode}
+%
+% SYNTAX for syntax rules
+%
+% `syntax' environment: used for syntax rules --- even (once!) for VDM.
+% \begin{macrocode}
+\def\syntax{\z@outnonbox\halign\bgroup
+ \zstrut$\@lign##$\hfil &\hfil$\@lign{}##{}$\hfil
+ &$\@lign##$\hfil &\qquad\@lign-- ##\hfil\cr}
+\let\endsyntax=\endzed
+% \end{macrocode}
+%
+% \subsection{Boxed environments}
+%
+%
+% SCHEMA schema definitions
+%
+% \begin{macrocode}
+\def\schema#1{\z@inoutbox\z@topline{$\,#1\,$}}
+\def\endschema{\z@botline \endzed \z@makeinner \z@nopar}
+% \end{macrocode}
+%
+% ANONSCHEMA schema with no name
+%
+% \begin{macrocode}
+\@namedef{anonschema}{\leftnamesfalse\z@inoutbox\z@topline{}}
+\expandafter\let\csname endanonschema\endcsname=\endschema
+% \end{macrocode}
+%
+% GENSCHEMA generic schema definitions
+%
+% \begin{macrocode}
+\def\genschema#1#2{\z@inoutbox\z@topline{$\,#1\:[#2]\,$}}
+\let\endgenschema=\endschema
+% \end{macrocode}
+%
+% AXDEF `liberal' axiomatic definitions
+%
+% \begin{macrocode}
+\def\axdef{\z@inoutbox}
+\def\endaxdef{\endzed\z@makeinner}
+% \end{macrocode}
+%
+% UNIQDEF `unique' axiomatic definitions
+%
+% \begin{macrocode}
+\def\uniqdef{\leftnamesfalse\z@inoutbox\z@dbltopline{}}
+\let\enduniqdef=\endschema
+% \end{macrocode}
+%
+% GENDEF 'generic' axiomatic definitions
+%
+% HACK TO MAKE IT COMPATIBLE WITH FUZZ.STY
+% \begin{macrocode}
+\def\gendef{\@ifnextchar[{\z@gendef}{\z@@gendef}}
+\def\z@gendef[#1]{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,[#1]\,$}}
+\def\z@@gendef#1{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,[#1]\,$}}
+\let\endgendef=\endschema
+% \end{macrocode}
+%
+% GENGENDEF generic contents 'generic' axiomatic definitions
+%
+% Hack to provide syntax-oriented display boxes
+% \begin{macrocode}
+\def\gengendef{\@ifnextchar[{\z@gengendef}{\z@@gengendef}}
+\def\z@gengendef[#1]{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,#1\,$}}
+\def\z@@gengendef#1{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,#1\,$}}
+\let\endgengendef=\endschema
+% \end{macrocode}
+%
+% CLASS
+%
+% \begin{macrocode}
+\def\class#1{\z@leavevmode\z@makeouter\z@inclasstrue
+ \z@boxenv\z@topline{$\,#1\,$}}
+\let\endclass\endschema
+% \end{macrocode}
+%
+% OP
+%
+% \begin{macrocode}
+\def\op{\z@inclasscheck\schema}
+\let\endop\endschema
+% \end{macrocode}
+%
+% STATE
+%
+% \begin{macrocode}
+\def\state{\z@inclasscheck\anonschema}
+\let\endstate\endschema
+% \end{macrocode}
+%
+% INIT
+%
+% \begin{macrocode}
+\def\init{\z@inclasscheck\schema{\Init}}
+\let\endinit\endschema
+% \end{macrocode}
+%
+% CONST
+%
+% \begin{macrocode}
+\let\const\axdef
+\let\endconst\endaxdef
+% \end{macrocode}
+%
+% TYPE
+%
+% \begin{macrocode}
+\def\type{\z@inclasscheck}
+\let\endtype\relax
+% \end{macrocode}
+%
+%\subsection{Other environments}
+%
+% SIDEBYSIDE
+%
+% This should support an arbitary number of columns
+% |\zedindent|'s proportion of |\linewidth| gives a practical limit
+%
+% \begin{macrocode}
+\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
+ \oz@parbox[t]{\linewidth}\bgroup\z@wide}
+%
+\def\nextside{\egroup\hss\oz@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}
+% \end{macrocode}
+%
+% ZPAR
+%
+% \begin{macrocode}
+\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\oz@parbox[b]{\linewidth}\bgroup\hfil\break}
+\def\endzpar{\egroup$$\z@makeinner\z@nopar}
+% \end{macrocode}
+%
+% CLASSCOM
+%
+% \begin{macrocode}
+\def \classcom{\zpar\sf}
+\let \endclasscom=\endzpar
+% \end{macrocode}
+%
+% PROOF
+%
+% \begin{macrocode}
+\def\proof{\zpar$\PR$\zpar}
+\def\endproof{\endzpar\endzpar}
+% \end{macrocode}
+%
+% Additional auxiliary macros
+%
+% \begin{macrocode}
+\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}}
+% \end{macrocode}
+%
+% OZ FUZZ
+%
+% |\defs| ==
+% |\sdef| |\defs|
+%
+% \begin{macrocode}
+\def\fuzzcompatible{%
+\let\defs\sdef
+\let\empty\emptyset
+}
+%
+%</package>
+% \end{macrocode}
+% \Finale
+\endinput