path: root/Master/texmf-dist/source/latex/objectz/oz.dtx

\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