summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/objectz
diff options
context:
space:
mode:
authorNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
committerNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
commite0c6872cf40896c7be36b11dcc744620f10adf1d (patch)
tree60335e10d2f4354b0674ec22d7b53f0f8abee672 /macros/latex/contrib/objectz
Initial commit
Diffstat (limited to 'macros/latex/contrib/objectz')
-rw-r--r--macros/latex/contrib/objectz/catalog7
-rw-r--r--macros/latex/contrib/objectz/makefile6
-rw-r--r--macros/latex/contrib/objectz/manifest9
-rw-r--r--macros/latex/contrib/objectz/oz.dtx1613
-rw-r--r--macros/latex/contrib/objectz/oz.ins53
-rw-r--r--macros/latex/contrib/objectz/ozguide.pdfbin0 -> 279519 bytes
-rw-r--r--macros/latex/contrib/objectz/ozguide.tex1311
-rw-r--r--macros/latex/contrib/objectz/oztest.tex206
-rw-r--r--macros/latex/contrib/objectz/readme45
9 files changed, 3250 insertions, 0 deletions
diff --git a/macros/latex/contrib/objectz/catalog b/macros/latex/contrib/objectz/catalog
new file mode 100644
index 0000000000..7edc81a9fc
--- /dev/null
+++ b/macros/latex/contrib/objectz/catalog
@@ -0,0 +1,7 @@
+Name: objectz
+Problems-To: s.rahtz@elsevier.co.uk
+Author: Sebastian Rahtz <s.rahtz@elsevier.co.uk>
+Date: 199r/01/06
+Version: 2.42
+Description: LaTeX package for typesetting Object Z schemas
+
diff --git a/macros/latex/contrib/objectz/makefile b/macros/latex/contrib/objectz/makefile
new file mode 100644
index 0000000000..edb8e0f58a
--- /dev/null
+++ b/macros/latex/contrib/objectz/makefile
@@ -0,0 +1,6 @@
+oz:
+ tex oz.ins
+ latex oz.dtx
+
+clean:
+ -rm *.aux *.toc *.sty *.dvi *.log *.tmp
diff --git a/macros/latex/contrib/objectz/manifest b/macros/latex/contrib/objectz/manifest
new file mode 100644
index 0000000000..e68ae4938e
--- /dev/null
+++ b/macros/latex/contrib/objectz/manifest
@@ -0,0 +1,9 @@
+total 112
+-rw-r--r-- 1 srahtz 191 Aug 6 10:27 catalog
+-rw-r--r-- 1 srahtz 79 Aug 6 10:27 makefile
+-rw-r--r-- 1 srahtz 0 Jan 7 11:49 manifest
+-rw-r--r-- 1 srahtz 54861 Nov 22 11:12 oz.dtx
+-rw-r--r-- 1 srahtz 1272 Aug 6 10:27 oz.ins
+-rw-r--r-- 1 srahtz 41883 Aug 6 10:27 ozguide.tex
+-rw-r--r-- 1 srahtz 10865 Aug 6 10:27 oztest.tex
+-rw-r--r-- 1 srahtz 1763 Jan 7 11:45 readme
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
diff --git a/macros/latex/contrib/objectz/oz.ins b/macros/latex/contrib/objectz/oz.ins
new file mode 100644
index 0000000000..5e8ce21167
--- /dev/null
+++ b/macros/latex/contrib/objectz/oz.ins
@@ -0,0 +1,53 @@
+% \iffalse
+% LaTex2e Oz style for typesetting Object Z
+% \fi
+\def\fileversion{1}
+\def\filedate{1993/12/23}
+%
+% \StopEventually{}
+%
+% As always we begin by identifying the latest version of this file
+% on the VDU and in the {\sf log} file.
+% \begin{macrocode}
+\def\batchfile{oz.ins}
+\input docstrip.tex
+\preamble
+
+Copyright (C) 1993 by Sebastian Rahtz
+All rights reserved.
+
+This file is part of the PSNFSS2e package.
+\endpreamble
+
+\def\batchfile{oz.dst} % ignored in distribution
+\input docstrip.tex % ignored in distribution
+
+\keepsilent
+
+\preamble
+Copyright (C) 1993 Sebastian Rahtz. All rights reserved.
+This is a generated file for Object Z. Permission is granted to to
+customize the declarations in this file to serve the needs of your
+installation. However, no permission is granted to distribute a
+modified version of this file under its original name.
+
+\endpreamble
+
+\Msg{*** Generating style file for Oz ***}
+
+\generateFile{oz.sty}{f}{
+ \from{oz.dtx}{package}}
+
+
+\Msg{***********************************************************}
+\Msg{*}
+\Msg{* To finish the installation you have to move the}
+\Msg{* file oz.sty into a directory searched by TeX}
+\Msg{*}
+\Msg{***********************************************************}
+
+
+\endinput
+
+
+
diff --git a/macros/latex/contrib/objectz/ozguide.pdf b/macros/latex/contrib/objectz/ozguide.pdf
new file mode 100644
index 0000000000..0a54b26d83
--- /dev/null
+++ b/macros/latex/contrib/objectz/ozguide.pdf
Binary files differ
diff --git a/macros/latex/contrib/objectz/ozguide.tex b/macros/latex/contrib/objectz/ozguide.tex
new file mode 100644
index 0000000000..9932d6dc0e
--- /dev/null
+++ b/macros/latex/contrib/objectz/ozguide.tex
@@ -0,0 +1,1311 @@
+\errorcontextlines=20
+\documentclass[a4paper]{article}
+\advance\textwidth by 1in
+\advance\textheight by 1in
+\advance\oddsidemargin by -0.5in
+\advance\topmargin by -0.5in
+\usepackage{oz}
+\usepackage{example}
+\usepackage{multicol}
+%
+% just ignore any over- or under-full hboxes
+% this document uses most of the (physical) page and isn't spread
+% out either. This may make it slightly harder to read first time
+% through, but makes it more suitable for later reference.
+%
+% before we start, let's make a few definitions
+%
+\makeatletter
+%\def\example{\begin{sidebyside}}
+%\def\verbpart{\nextside\small\vspace*{-1ex}\begin{quote}\begin{verbatim}}
+%\def\endexample{\end{quote}\vspace*{-2ex}\end{sidebyside}\vspace*{-3ex}\ignorespaces}
+\def\symbol#1{#1 & \tt\string#1}
+\def\symbols{\@ifnextchar[{\@symbols}{\@symbols[0]}}
+\def\@symbols[#1]{\interzedlinepenalty=\interdisplaylinepenalty\z@env
+ \openup #1\jot
+ \halign\bgroup\zstrut\hbox to 3.8em{$##$\hss}\tabskip=0pt&##\hss\cr
+ \noalign{\vskip-#1\jot}}% equal vspace above and below argue display
+\let\endsymbols=\endzed
+\makeatother
+%
+\begin{document}
+\begin{center}
+{\Large\bf Printing Z and Object-Z \LaTeX\ documents}\\[2.5ex]
+{\em Paul King}\\[1ex]
+Department of Computer Science\\
+University of Queensland\\
+Australia, 4072\\
+king@batserver.cs.uq.oz.au\\[1ex]
+May 29, 1990
+\end{center}
+
+\section{Introduction}
+This note describes a package of \LaTeX\ macros for printing
+Z and Object-Z specifications. The macros and this note are
+based originally on Mike Spivey's \verb'zed.sty' macros and documentation.
+The package does several related things for you:
+\begin{itemize}
+\item It loads extra fonts and defines mnemonics
+ for the Z symbols they contain.
+\item It defines macros for some Z symbols (e.g. $\pinj$) which
+ don't appear in any of our fonts.
+\item It fixes the way \TeX\ sets letters in mathematical formulas so
+ that multi-character identifiers look better.
+\item It provides various brands of `boxed mathematics'
+ which appear in Z and Object-Z specifications.
+\end{itemize}
+
+The package is kept in a file {\tt oz.sty}
+in the directory \verb|/usr/local/lib/tex/localinputs|.
+This directory should be mentioned in your \verb|TEXINPUTS| shell variable.
+To use the macros you just begin your \LaTeX\ document with something like:
+\begin{quote}
+\begin{verbatim}
+\documentstyle[11pt,oz]{article}
+\end{verbatim}
+\end{quote}
+\vspace*{-1.5ex}
+
+\section{Schema Boxes}
+
+The example below shows a schema on the left and what you
+need to say to get it on the right.
+
+\begin{example}
+\begin{schema}{BirthdayBook}
+ known: \pset NAME \\
+ birthday: NAME \pfun DATE
+\ST
+ known = \dom birthday
+\end{schema}
+\end{example}
+
+The command \verb|\ST| (read `Such That') is the same as the previously used
+command \verb|\where| which has been kept as an alias for upward compatibility.
+If you want a schema with no name, just a horizontal rule at the top,
+use the \verb|schema*| environment instead.
+You can set various parameters (see Section 7) to change the box style,
+for example:
+
+\begin{example}
+$BirthdayBook \sdef \lsch ... \rsch$
+\end{example}
+
+A generic schema is produced as follows.
+
+\begin{example}
+\begin{genschema}{Pool}{RESOURCE}
+owner : RESOURCE \pfun USER \\
+free : \pset RESOURCE
+\ST
+(\dom owner) \uni free = RESOURCE \\
+(\dom owner) \int free = \emptyset
+\end{genschema}
+\end{example}
+
+\section{Axiomatic definitions}
+
+A `liberal' axiomatic definition is produced as follows.
+
+\begin{example}
+\begin{axdef}
+limit : \nat
+\ST
+limit \leq 65536
+\end{axdef}
+\end{example}
+
+A `generic' axiomatic definition is produced as follows.
+
+\begin{example}
+\begin{gendef}{X,Y}
+first : X \prod Y \tfun X
+\ST
+\all x : X; y : Y \dot first(x,y) = x
+\end{gendef}
+\end{example}
+
+A `unique' axiomatic definition is produced as follows.
+
+\begin{example}
+\begin{uniqdef}
+\pi : \real
+\ST
+\pi = 3.14159265\ldots
+\end{uniqdef}
+\end{example}
+
+\section{Object-Z Class Boxes}
+
+Object-Z allows class types to be defined using a box very similar to
+the schema box previously described. It allows the previously
+described boxed environments (as well as nested sub-classes) to be
+placed within a class box. In addition, special names can be used for
+some of the boxed-environments when they appear within a class box.
+The following example illustrates a class definition.
+
+\begin{example}
+\begin{class}{Shape}
+\also
+colour : Colour \\
+\begin{axdef}
+perim : \real
+\ST
+perim > 0
+\end{axdef} \\
+\begin{classcom}
+This class has 2 constants
+$colour$ and $perim$.
+\end{classcom} \\
+\begin{state}
+x, y : \real
+\end{state} \\
+\begin{init}
+x = y = 0
+\end{init} \\
+\begin{op}{Translate}
+\Delta (x,y) \\
+dx?, dy? : \real
+\ST
+x' = x + dx? \\
+y' = y + dy?
+\end{op}
+\end{class}
+\end{example}
+
+The \verb|classcom| environment hasn't been seen before.
+It creates a paragraph of text with the same margins as used
+for schemas and other Z environments. It uses a special font
+intended for use when placing comments inside classes.
+A similar environment, \verb|zpar|, uses the same margins
+but with the normal roman font.
+
+The \verb|\begin{init}| command is an abbreviation for
+\verb|\begin{schema}{\Init}|. Similarly \verb|\begin{state}|
+is a more meaningful synonym for \verb|\begin{schema*}|.
+
+You will be given \LaTeX\ warning messages if you try to
+use a \verb|state| environment outside of a class box
+or if you try to place an environment such as \verb|syntax|
+inside a class. You can ask for additional help in these
+cases using the normal \LaTeX\ \verb|h| or \verb|H| help commands.
+If you proceed with \LaTeX ing, the macros will attempt to
+do the best they can to do what you probably intend, even though
+you are violating the recommended nesting guidelines.
+
+\section{Controlling the Spacing within Equations and Boxes}
+
+Most of the special Z symbols are defined
+in a way that allows \TeX\ to space them out correctly.
+Sometimes, however, you'll need to give \TeX\ a helping hand if
+you want it to get the spacing right. For example, to get $map\,f$
+you need to type \verb|map\,f|. The \verb|\,| gives you a thin space:
+if this is omitted, the input \verb|map f| gives
+$map f$, because \TeX\ ignores spaces in math mode.
+
+Sometimes it is useful to indent the left margin to emphasis
+the logical structure of the predicate.
+The command \verb|\t1| does this by making the corresponding
+line in the output have one helping of indentation.
+As things get more nested, you can say \verb|\t2|, \verb|\t3|, and so on.
+But if you should ever get beyond \verb|t9|, you'll need to use braces
+around the argument: \verb|\t{10}|, and you'd better look for some way
+to simplify your specification!
+These little tab marks might look different to normal tabs
+but are never the less convenient. They're short,
+and they don't get longer as the tabbing gets deeper, within reason,
+so they can be tucked in neatly on the left, well away from the maths.
+The size of `helping' you get with \verb|\t| is determined by
+the \verb|\zedtab| parameter (see Section 7).
+
+If you want a more powerful aligning mechanism than tabbing
+then you can use the margin stack as shown in the example below.
+The command \verb|\M| sets the future left margin to the current
+horizontal position and pushes the old value onto a margin stack.
+The command \verb|\O| resets the left margin to its previous value
+(which is popped off the stack).
+
+\begin{example}
+\begin{schema}{Test}
+x, y : \nat
+\ST
+x + 1/x = 0 \imp \M y + 1/y = 0 \\
+y = x \O \\
+\end{schema}
+\end{example}
+
+If a schema or other box contains more than one predicate below the
+line, it often looks better to add a tiny vertical space between
+them, as in this example:
+
+\begin{example}
+\begin{schema}{AddBirthday}
+ \Delta BirthdayBook \\
+ n?: NAME \\
+ d?: DATE
+\ST
+ n? \nem known
+\also
+ birthday'=birthday \uni \{n? \map d?\}
+\end{schema}
+\end{example}
+
+This is done with the command \verb|\also|, which behaves syntactically
+like \verb|\ST|.
+The command \verb|\also| is provided {\em instead\/} of the
+optional argument to \verb|\\|
+which \LaTeX\ provides in other environments.
+If larger vertical spacing is required, the commands
+\verb|\Also| and \verb|\ALSO| may be used (giving 2 and 4 times
+as much space as \verb|\also| respectively).
+
+Normally, the contents of a schema box are kept on a single page.
+For large schemas it may be necessary to split the box across pages.
+You must specify which places are suitable for splitting using one of
+\verb|\zbreak|, \verb|\Zbreak| or \verb|\ZBREAK|. If no split is
+performed at this point, a vertical space will be added as if the
+user had typed \verb|\also|, \verb|\Also|, or \verb|\ALSO| respectively.
+You can also use the \verb|\znewpage| command to force a page break within
+a box. (These breaking facilities will hopefully never be needed for schemas,
+but may become necessary for class specifications.)
+
+\section{Other Display Environments}
+
+The \verb|zed| environment can be used to set multi-line formulas without
+an enclosing box: it is useful for given-set declarations, theorems, and the
+miscellaneous bits of mathematics that don't come in a box:
+
+\vspace{-1ex}\begin{example}
+\begin{zed}
+ \all n: \nat \dot \\
+\t1 n+n \mem even.
+\end{zed}
+\end{example}
+
+The formula \verb|\begin{zed} ... \end{zed}| may be abbreviated to
+\verb|\[ ... \]|; the \verb|zed| environment is a generalization of the
+\verb|displaymath| environment of \LaTeX, so this redefinition of
+commands is fairly benign. Notice that the maths is set flush left on the
+same indentation as schemas and their friends.
+Here too you can use \verb|\also| for a little extra space
+between lines.
+
+For algebraic-style proofs, there is the \verb|argue| environment.
+This is like the \verb|zed| environment, but the separation between
+lines is increased a little, and page breaks may occur between lines.
+When the left-hand side is long this style wastes less space
+than the \LaTeX\ \verb|eqnarray| style.
+The intended use is for arguments like this:
+\begin{argue}
+ rev(append(cons(x,s),t)) \\
+\t1 = rev(cons(x,append(s,t))) \\
+\t1 = append(rev(append(s,t)),cons(x,nil)) \\
+\t1 = append(append(rev(t),rev(s)),cons(x,nil))
+ \quad \hbox{by hypothesis} \\
+\t1 = append(rev(t),append(rev(s),cons(x,nil))) \\
+\t1 = append(rev(t),rev(cons(x,s))).
+\end{argue}
+Here is the input:
+\begin{quote}
+\begin{verbatim}
+\begin{argue}
+ rev(append(cons(x,s),t)) \\
+\t1 = rev(cons(x,append(s,t))) \\
+\t1 = append(rev(append(s,t)),cons(x,nil)) \\
+\t1 = append(append(rev(t),rev(s)),cons(x,nil))
+ \quad \hbox{by hypothesis} \\
+\t1 = append(rev(t),append(rev(s),cons(x,nil))) \\
+\t1 = append(rev(t),rev(cons(x,s))).
+\end{argue}
+\end{verbatim}
+\end{quote}
+
+The example below shows an inference rule (the optional argument
+to \verb|\derive| gives a side-condition of the rule):
+
+\vspace{-1ex}\begin{example}
+\begin{infrule}
+ \Gamma \shows P
+\derive[x \nem freevars(\Gamma)]
+ \Gamma \shows \all x \dot P
+\end{infrule}
+\end{example}
+
+The \verb|syntax| environment is used for making displays like this:
+
+\begin{syntax}
+ EXPR & \ddef & IDENT & identifier \\
+ & \bbar & EXPR\;EXPR & application \\
+ & \bbar & \lambda IDENT \dot EXPR & lambda-abstraction.
+\end{syntax}
+from input like this:
+\begin{quote}
+\begin{verbatim}
+\begin{syntax}
+ EXPR & \ddef & IDENT & identifier \\
+ & \bbar & EXPR\;EXPR & application \\
+ & \bbar & \lambda IDENT \dot EXPR & lambda-abstraction.
+\end{syntax}
+\end{verbatim}
+\end{quote}
+
+This kind of thing is useful when you're describing a language,
+and it can also be used for data-type definitions as shown below.
+The optional final column was omitted below by leaving out the third \verb|&|.
+
+\begin{example}
+\begin{syntax}
+TYPE & \ddef & givenT \lang NAME \rang \\
+& \bbar & powerT \lang TYPE \rang \\
+& \bbar & tupleT \lang \seq TYPE \rang \\
+& \bbar & schemaT \lang IDENT \ffun TYPE \rang \\
+& \bbar & classT \lang IDENT \ffun ClassAttr \rang
+\end{syntax}
+\end{example}
+
+This can be compared with the layout adopted by the UQ Z editor (version 1).
+
+\begin{example}
+\begin{zed}
+TYPE \ddef \M givenT \lang NAME \rang \\
+\bbar powerT \lang TYPE \rang \\
+\bbar tupleT \lang \seq TYPE \rang \\
+\bbar schemaT \lang IDENT \ffun TYPE \rang \\
+\bbar classT \lang IDENT \ffun ClassAttr \rang \O
+\end{zed}
+\end{example}
+
+The {\tt sidebyside} environment allows a display as shown in the
+first two columns below to be produced from the text of the third column.
+Note the use of the \verb|\comment| command.
+
+\begin{example}
+\begin{sidebyside}
+\begin{schema}{Schema}
+\comment*{declarations}
+\ST
+a < b \comment{pred-1} \\
+aaaaa < bbbbb \comment{pred-2}
+\end{schema}
+\nextside
+\begin{zpar}
+This is a paragraph which has the same
+margins as the standard schemas do.
+\end{zpar}
+\end{sidebyside}
+\end{example}
+
+In fact, this environment was used throughout this note to
+display the examples beside the required input text.
+Incidentally, the above example shows that \verb|sidebyside|
+environments can be nested; so what the author of this note typed
+to get the above display was:
+
+\begin{quote}
+\begin{verbatim}
+\begin{sidebyside}
+ \begin{sidebyside}
+ ...
+ \nextside
+ ...
+ \end{sidebyside}
+\nextside
+ ...
+\end{sidebyside}
+\end{verbatim}
+\end{quote}
+
+This resulted in the first two columns being equally spaced and
+together taking up as much space as the third column.
+You can have more than 2 columns without nesting by specifying an optional
+parameter to \verb|sidebyside|. For example, the display below has three
+equally spaced columns obtained using \verb|\begin{sidebyside}[3]|.
+
+ \begin{sidebyside}[3]
+ \begin{schema}{BirthdayBook}
+ known: \pset NAME \\
+ birthday: NAME \pfun DATE
+ \ST
+ known = \dom birthday
+ \end{schema}
+ \nextside
+ \begin{schema}{BirthdayBook}
+ known: \pset NAME \\
+ birthday: NAME \pfun DATE
+ \ST
+ known = \dom birthday
+ \end{schema}
+ \nextside
+ \begin{zpar}
+Don't get carried away with \verb|sidebyside|
+ like this example does.
+ \end{zpar}
+ \end{sidebyside}
+
+\section{Style Parameters}
+
+\begin{description}
+\item[\tt\string\zedindent] The (horizontal) indentation for mathematical text.
+ By default, this is the same as \verb|\leftmargini|, the indentation
+ used for list environments.
+\item[\tt\string\zedleftsep] The (horizontal) space between the vertical line on the left
+ of schemas, etc., and the maths inside. The default is 1em.
+\item[\tt\string\zedtab] The unit of indentation used by \verb|\t|. The default
+ is 2em.
+\item[\tt\string\zedbar] The length of the horizontal bar in the middle of a
+ schema. The default is 8em.
+\item[\tt\string\leftschemas] A declaration which makes schema names be
+ set flush left. Use it in the document preamble.
+\item[\tt\string\zedlinethickness] The thickness of the lines that make up
+ schema and class boxes. You can change the thickness
+ with a command such as \verb|\zedlinethickness=0.1pt|. This may
+ be useful if you are creating overhead slides.
+ \begin{description}
+ \makeatletter
+ \item[0.1pt] \zedlinethickness=0.1pt
+ ~\hbox to 4cm{\z@hrulefill}
+ \item[0.4pt] \zedlinethickness=0.4pt
+ ~\hbox to 4cm{\z@hrulefill}~~~(The default)
+ \item[\hphantom{0.}1pt] \zedlinethickness=1pt
+ ~\hbox to 4cm{\z@hrulefill}
+ \end{description}
+\item[\tt\string\baselinestretch] The spacing for the text part of your
+ document. It doesn't change the spacing within Z environments. It's
+ default value is 1. A command such as \verb|\def\baselinestretch{2}|
+ will make your text double spaced, but not your Z environments.
+\item[\tt\string\zedbaselinestretch] The spacing for the Z environment
+ part of your document. It's default value is 1.
+\item[\tt\string\zedsize] The size of the material within the Z
+ part of your document. It doesn't affect the remainder of your document.
+ For example, \verb|\zedsize{\large}| will give you large Z symbols
+ and equations but will not affect the size of the surrounding text.
+\item[\tt\string\zedcornerheight] The height of `corners' that can be placed
+ on the right hand side of the top and bottom lines of schema and class
+ boxes. The default is 0em (i.e. no corners).
+\end{description}
+
+\section{Symbols}
+
+Multi-letter identifiers have been changed to look
+better than they do with vanilla \LaTeX: instead of
+$\mathit{specifications}$, you get $specifications$.
+The letters haven't been spread apart, and the
+ligature $fi$ has been used.
+
+Almost all of the mathematical symbols of \LaTeX\ can be used;
+some have been redefined---usually to fix the spacing so that it is
+suitable for Z specifications.
+The commands for obtaining additional symbols are listed below.
+Sometimes more than one command may produce a symbol you
+require. You should use the one that seems to be designed for the
+context you have in mind. This is because the spacing around (and size of)
+symbols has been chosen for their typical context.
+
+Throughout the lifetime of these macros a number of alternate control
+sequences for any symbol may have existed. A list of aliases has been
+set up so that old commands may still be used. It is
+recommended however that you stick to the recommended command
+names for symbols as these names may be supported by other tools.
+Within the table below non-recommended aliases are surrounded by
+brackets, e.g., \verb|(\power)|.
+\begin{multicols}{2}
+\setcounter{secnumdepth}{2}
+\zedindent=0.2\zedindent
+\subsection{Special Z Notation}
+\vspace*{-0.5ex}
+\subsubsection{Numbers}
+\vspace*{-2.5ex}
+\begin{symbols}
+\nat & \verb' \nat' \\
+\natone & \verb' \natone (\nplus)' \\
+\integer & \verb' \integer (\num)' \\
+\real & \verb' \real' \\
+\div~\mod & \verb' \div \mod' \\
+i^n & \verb' i^n i\expon n' \\
+\succ & \verb' \succ' \\
+%\prec & \verb' \prec' \\
+=~\neq & \verb' = \neq' \\
+<~\leq~\leqslant & \verb' < \leq \leqslant' \\
+>~\geq~\geqslant & \verb' > \geq \geqslant' \\
+*\,/\,+ - & \verb' * / + -' \\
+\end{symbols}
+\subsubsection{Logic}
+\vspace*{-2.5ex}
+\begin{symbols}
+\lnot & \verb'\lnot' \\
+\land & \verb'\land (\wedge)' \\
+\lor & \verb'\lor (\vee)' \\
+\all & \verb'\all (\forall)' \\
+\exi & \verb'\exi (\exists)' \\
+\exi_1 & \verb'\exione' \\
+\nexi & \verb'\nexi (\nexists)' \\
+\dot & \verb'@ \dot (\spot)' \\
+%\cond & \verb'\cond' \\
+\imp & \verb'\imp (\implies)' \\
+\iff & \verb'\iff' \\
+\true & \verb'\true' \\
+\false & \verb'\false' \\
+\bool & \verb'\bool' \\
+\end{symbols}
+\subsubsection{Sets}
+\vspace*{-2.5ex}
+\begin{symbols}
+\{~~\cbar~~\} & \verb' \{ \cbar \}' \\
+\emptyset & \verb' \emptyset' \\
+\varemptyset & \verb' \varemptyset' \\
+\mem & \verb' \mem (\in)' \\
+\nmem & \verb' \nem (\nmem \notin)' \\
+\pset & \verb' \pset (\power)' \\
+\fset & \verb' \fset (\finset)' \\
+\psetone~~\fsetone & \verb' \fsetone \psetone' \\
+\uni & \verb' \uni (\union)' \\
+\int & \verb' \int (\inter)' \\
+\psubs & \verb' \psubs (\subset)' \\
+\subs & \verb' \subs (\subseteq)' \\
+\psups & \verb' \psups (\supset)' \\
+\sups & \verb' \sups (\supseteq)' \\
+\prod & \verb' \prod (\cross)' \\
+\min~\max & \verb' \min \max' \\
+\# & \verb' \#' \\
+\duni & \verb' \duni (\dunion)' \\
+\dint & \verb' \dint (\dinter)' \\
+\upto & \verb' \upto' \\
+\end{symbols}
+
+\subsubsection{Relations and Functions}
+\vspace*{-2.5ex}
+\begin{symbols}[0.1]
+\lambda~~~\mu & \verb'\lambda \mu' \\
+\dom & \verb'\dom' \\
+\ran & \verb'\ran' \\
+\dres & \verb'\dres' \\
+\dsub & \verb'\dsub (\ndres)' \\
+\rres & \verb'\rres' \\
+\rsub & \verb'\rsub (\nrres)' \\
+\fovr & \verb'\fovr' \\
+\cmp & \verb'\cmp' \\
+\fcmp & \verb'\fcmp (\comp)' \\
+(\!|~~~|\!) & \verb'\limg \rimg' \\
+\id & \verb'\id' \\
+R\inv & \verb'R^{-1} R\inv' \\
+R^+ & \verb'R^+ R\tcl' \\
+R^* & \verb'R^* R\rtcl' \\
+R^k & \verb'R^k R\iter k' \\
+iter\,0\,R & \verb'iter \, 0 \, R' \\
+\map & \verb'\map' \\
+\rel & \verb'\rel' \\
+\tfun & \verb'\tfun (\fun)' \\
+\tinj & \verb'\tinj (\inj)' \\
+\tsur & \verb'\tsur (\surj)' \\
+\pfun & \verb'\pfun' \\
+\pinj & \verb'\pinj' \\
+\psur & \verb'\psur (\psurj)' \\
+\ffun & \verb'\ffun' \\
+\finj & \verb'\finj' \\
+\bij & \verb'\bij' \\
+\end{symbols}
+\subsubsection{Sequences}
+\vspace*{-2.5ex}
+\begin{symbols}
+\seq & \verb' \seq' \\
+\seqone & \verb' \seqone' \\
+\emptyseq & \verb' \emptyseq' \\
+\lseq~~~\rseq & \verb' \lseq \rseq' \\
+\head~~\tail & \verb' \head \tail' \\
+\front~~\last & \verb' \front \last' \\
+\rev & \verb' \rev' \\
+\next & \verb' \next' \\
+\inseq & \verb' \inseq' \\
+\prefix & \verb' \prefix' \\
+\suffix & \verb' \suffix' \\
+\squash & \verb' \squash' \\
+\cat & \verb' \cat' \\
+\dcat & \verb' \dcat' \\
+\dcmp & \verb' \dcmp' \\
+\dovr & \verb' \dovr' \\
+\ires & \verb' \ires' \\
+\sres & \verb' \sres \filter' \\
+\partitions & \verb' \partitions' \\
+\disjoint & \verb' \disjoint' \\
+\end{symbols}
+
+\subsubsection{Schemas}
+\vspace*{-2.5ex}
+\begin{symbols}
+\Delta & \verb'\Delta' \\
+\equiv~~\Xi & \verb'\equiv \Xi' \\
+\pred & \verb'\pred' \\
+\pre & \verb'\pre' \\
+\post & \verb'\post' \\
+\project & \verb'\zproject \project' \\
+\zand & \verb'\zand' \\
+\zor & \verb'\zor' \\
+\zcmp & \verb'\zcmp (\semi)' \\
+\zexi & \verb'\zexi' \\
+\zall & \verb'\zall' \\
+\znot & \verb'\znot' \\
+\zhide & \verb'\zhide (\hide)' \\
+\zfor & \verb'\zfor' \\
+\zimp & \verb'\zimp' \\
+\zeq & \verb'\zeq' \\
+\zovr & \verb'\zovr' \\
+\zpipe & \verb'\zpipe' \\
+\theta & \verb'\theta' \\
+\lsch~~\zbar~~\rsch & \verb'\lsch \zbar \rsch' \\
+.. & \verb'.' \\
+\end{symbols}
+\subsubsection{Bags}
+\vspace*{-2.5ex}
+\begin{symbols}
+\lbag~~~\rbag & \verb'\lbag \rbag' \\
+\bag & \verb'\bag' \\
+\emptybag & \verb'\emptybag' \\
+\items & \verb'\items' \\
+\bagcount & \verb'\bagcount' \\
+\buni & \verb'\buni' \\
+\inbag & \verb'\inbag' \\
+\end{symbols}
+\subsubsection{Definitions and Declarations}
+\vspace*{-2.5ex}
+\begin{symbols}
+::= & \verb'\ddef' \\
+\bbar & \verb'\bbar' \\
+== & \verb'\defs' \also
+\widehat= & \verb'\sdef' \also
+\triangleq & \verb'\varsdef' \\
+,~~\semicolon~~: & \verb', ; :' \\
+\lang~~~\rang & \verb'\lang \rang' \\
+\end{symbols}
+\subsubsection{Miscellaneous}
+\vspace*{-2.5ex}
+\begin{symbols}[0]
+[~~~] & \verb'[ ]' \\
+(~~~) & \verb'( )' \\
+!~~~? & \verb'! ?' \\
+\zlet & \verb'\zlet' \\
+\zwhere & \verb'\zwhere' \\
+\zin & \verb'\zin' \\
+\langle\!|~~~|\!\rangle & \verb'\lblot \rblot' \\
+\intern Bump & \verb'\intern Bump' \\
+\Init & \verb'\Init'\\
+\Exit & \verb'\Exit'
+\end{symbols}
+
+\subsection{Other Special Notation}
+\vspace*{-1ex}
+\subsubsection{Temporal Logic}
+\vspace*{-2.5ex}
+\begin{symbols}
+\always~\uptilnow & \verb'\always \uptilnow' \\
+~&\verb'(\henceforth)'\\
+\atnext~\atlast & \verb'\atnext \atlast' \\
+\eventually~\previously & \verb'\eventually \previously' \\
+\end{symbols}
+\subsubsection{Proofs}
+\vspace*{-2.5ex}
+\begin{symbols}[0.1]
+\TH & \verb' \TH' \\
+\PR & \verb' \PR' \\
+\LE & \verb' \LE' \\
+\ETH~\Qed & \verb' \qed (\ETH) \Qed' \\
+\QED~\BLACKQED & \verb' \QED \BLACKQED' \\
+\vdash & \verb' \shows (\thrm)' \\
+\vDash & \verb' \vDash' \\
+\refines & \verb' \refines' \\
+\weakrefine & \verb' \weakrefine' \\
+\end{symbols}
+\subsubsection{Object Theory}
+\vspace*{-2.5ex}
+\begin{symbols}
+\subclass & \verb'\subclass \isa' \\
+\weaksubclass & \verb'\weaksubclass \islikea' \\
+\supclass & \verb'\supclass' \\
+\weaksupclass & \verb'\weaksupclass' \\
+\hasa & \verb'\hasa \instantiates' \\
+\instancein & \verb'\instancein' \\
+\subtype~~\subtypeeq & \verb'\subtype \subtypeeq' \\
+\suptype~~\suptypeeq & \verb'\suptype \suptypeeq' \\
+\end{symbols}
+\subsubsection{Orders}
+\vspace*{-2.5ex}
+\begin{symbols}
+\mono & \verb' \mono' \\ % these lines fudged to give more spacing
+\torder & \verb' \torder' \\
+\porder & \verb' \porder' \\
+\end{symbols}
+\subsubsection{Word Styles}
+\vspace*{-2.5ex}
+\begin{symbols}[0.4]
+\word{word} & \verb'\word{word}' \\
+\keyword{word} & \verb'\keyword{word}' \\
+\boldword{word} & \verb'\boldword{word}' \\
+\underword{word} & \verb'\underword{word}' \\
+\underkeyword{word} & \verb'\underkeyword{word}' \\
+\underboldword{word} & \verb'\underboldword{word}' \\
+\String{word} & \verb'\String{word}' \\
+\STRING{word} & \verb'\STRING{word}' \\
+a \infix{rel} b & \verb'a \infix{rel} b' \\
+\end{symbols}
+
+\subsection{Special Letter Fonts}
+\vspace*{-1ex}
+\subsubsection{Greek}
+\vspace*{-2.5ex}
+\begin{symbols}
+\alpha & \verb'\alpha' \\
+\beta & \verb'\beta' \\
+\gamma~\Gamma & \verb'\gamma \Gamma' \\
+\delta~\Delta & \verb'\delta \Delta' \\
+\epsilon~\varepsilon & \verb'\epsilon \varepsilon' \\
+\zeta & \verb'\zeta' \\
+\eta & \verb'\eta' \\
+\theta~\vartheta~\Theta & \verb'\theta \vartheta \Theta' \\
+\iota & \verb'\iota' \\
+\kappa~\varkappa & \verb'\kappa \varkappa' \\
+\lambda~\Lambda & \verb'\lambda \Lambda' \\
+\mu & \verb'\mu' \\
+\nu & \verb'\nu' \\
+\xi~\Xi & \verb'\xi \Xi' \\
+\pi~\varpi~\Pi & \verb'\pi \varpi \Pi' \\
+\rho~\varrho & \verb'\rho \varrho' \\
+\sigma~\varsigma~\Sigma & \verb'\sigma \varsigma \Sigma' \\
+\tau & \verb'\tau' \\
+\upsilon~\Upsilon & \verb'\upsilon \Upsilon' \\
+\phi~\varphi~\Phi & \verb'\phi \varphi \Phi' \\
+\chi & \verb'\chi' \\
+\psi~\Psi & \verb'\psi \Psi' \\
+\omega~\Omega & \verb'\omega \Omega' \\
+\end{symbols}
+\subsubsection{Caligraphic}
+\vspace*{-2.5ex}
+\begin{symbols}
+\mathcal{A} & \verb'\mathcal{A}' \\
+\mathcal{B} & \verb'\mathcal{B}' \\
+\mathcal{C} & \verb'\mathcal{C}' \\
+\mathcal{D} & \verb'\mathcal{D}' \\
+\mathcal{E} & \verb'\mathcal{E}' \\
+\mathcal{F} & \verb'\mathcal{F}' \\
+\mathcal{G} & \verb'\mathcal{G}' \\
+\mathcal{H} & \verb'\mathcal{H}' \\
+\mathcal{I} & \verb'\mathcal{I}' \\
+\mathcal{J} & \verb'\mathcal{J}' \\
+\mathcal{K} & \verb'\mathcal{K}' \\
+\mathcal{L} & \verb'\mathcal{L}' \\
+\mathcal{M} & \verb'\mathcal{M}' \\
+\mathcal{N} & \verb'\mathcal{N}' \\
+\mathcal{O} & \verb'\mathcal{O}' \\
+\mathcal{P} & \verb'\mathcal{P}' \\
+\mathcal{Q} & \verb'\mathcal{Q}' \\
+\mathcal{R} & \verb'\mathcal{R}' \\
+\mathcal{S} & \verb'\mathcal{S}' \\
+\mathcal{T} & \verb'\mathcal{T}' \\
+\mathcal{U} & \verb'\mathcal{U}' \\
+\mathcal{V} & \verb'\mathcal{V}' \\
+\mathcal{W} & \verb'\mathcal{W}' \\
+\mathcal{X} & \verb'\mathcal{X}' \\
+\mathcal{Y} & \verb'\mathcal{Y}' \\
+\mathcal{Z} & \verb'\mathcal{Z}' \\
+\end{symbols}
+\subsubsection{BlackBoard Bold}
+\vspace*{-2.5ex}
+\begin{symbols}
+\mathbb A & \verb'\mathbb A' \\
+\mathbb B & \verb'\mathbb B' \\
+\mathbb C & \verb'\mathbb C' \\
+\mathbb D & \verb'\mathbb D' \\
+\mathbb E & \verb'\mathbb E' \\
+\mathbb F & \verb'\mathbb F' \\
+\mathbb G & \verb'\mathbb G' \\
+\mathbb H & \verb'\mathbb H' \\
+\mathbb I & \verb'\mathbb I' \\
+\mathbb J & \verb'\mathbb J' \\
+\mathbb K & \verb'\mathbb K' \\
+\mathbb L & \verb'\mathbb L' \\
+\mathbb M & \verb'\mathbb M' \\
+\mathbb N & \verb'\mathbb N' \\
+\mathbb O & \verb'\mathbb O' \\
+\mathbb P & \verb'\mathbb P' \\
+\mathbb Q & \verb'\mathbb Q' \\
+\mathbb R & \verb'\mathbb R' \\
+\mathbb S & \verb'\mathbb S' \\
+\mathbb T & \verb'\mathbb T' \\
+\mathbb U & \verb'\mathbb U' \\
+\mathbb V & \verb'\mathbb V' \\
+\mathbb W & \verb'\mathbb W' \\
+\mathbb X & \verb'\mathbb X' \\
+\mathbb Y & \verb'\mathbb Y' \\
+\mathbb Z & \verb'\mathbb Z' \\
+\end{symbols}
+\subsubsection{Miscellaneous}
+\vspace*{-2.5ex}
+\begin{symbols}
+\hslash & \verb'\hslash' \\
+\hbar & \verb'\hbar' \\
+\backepsilon & \verb'\backepsilon' \\
+\eth & \verb'\eth' \\
+\beth & \verb'\beth' \\
+\gimel & \verb'\gimel' \\
+\daleth & \verb'\daleth' \\
+\complement & \verb'\complement' \\
+\intercal & \verb'\intercal' \\
+\aleph & \verb'\aleph' \\
+\nabla & \verb'\nabla' \\
+\hbar & \verb'\hbar' \\
+\imath & \verb'\imath' \\
+\jmath & \verb'\jmath' \\
+\ell & \verb'\ell' \\
+\wp & \verb'\wp' \\
+\Re & \verb'\Re' \\
+\Im & \verb'\Im' \\
+\mho & \verb'\mho' \\
+\digamma & \verb'\digamma' \\
+\end{symbols}
+
+\subsection{Shapes}
+\vspace*{-2ex}
+\begin{symbols}
+\Box & \verb'\Box' \\
+\square & \verb'\square' \\
+\blacksquare & \verb'\blacksquare' \\
+\diamond & \verb'\diamond' \\
+\Diamond & \verb'\Diamond' \\
+\lozenge & \verb'\lozenge' \\
+\blacklozenge & \verb'\blacklozenge' \\
+\vartriangleright & \verb'\vartriangleright' \\
+\vartriangleleft & \verb'\vartriangleleft' \\
+\blacktriangledown & \verb'\blacktriangledown' \\
+\blacktriangleright & \verb'\blacktriangleright' \\
+\blacktriangleleft & \verb'\blacktriangleleft' \\
+\vartriangle & \verb'\vartriangle' \\
+\blacktriangle & \verb'\blacktriangle' \\
+\triangledown & \verb'\triangledown' \\
+\triangle & \verb'\triangle' \\
+\triangleleft & \verb'\triangleleft' \\
+\triangleright & \verb'\triangleright' \\
+\bigtriangleup & \verb'\bigtriangleup' \\
+\bigtriangledown & \verb'\bigtriangledown' \\
+\clubsuit & \verb'\clubsuit' \\
+\diamondsuit & \verb'\diamondsuit' \\
+\heartsuit & \verb'\heartsuit' \\
+\spadesuit & \verb'\spadesuit' \\
+\ast & \verb'\ast' \\
+\star & \verb'\star' \\
+\maltese & \verb'\maltese' \\
+\bigstar & \verb'\bigstar' \\
+\bigcirc & \verb'\bigcirc' \\
+\circ & \verb'\circ' \\
+\bullet & \verb'\bullet' \\
+\centerdot & \verb'\centerdot' \\
+\cdot & \verb'\cdot' \\
+\cdots & \verb'\cdots' \\
+\ldots & \verb'\ldots' \\
+\vdots & \verb'\vdots' \\
+\ddots & \verb'\ddots' \\
+\end{symbols}
+\subsubsection{Circled Operations}
+\vspace*{-2.5ex}
+\begin{symbols}
+\circledS & \verb'\circledS' \\
+\circledcirc & \verb'\circledcirc' \\
+\circledast & \verb'\circledast' \\
+\circleddash & \verb'\circleddash' \\
+\circledR & \verb'\circledR' \\
+\copyright & \verb'\copyright' \\
+\fovr & \verb'\fovr' \\
+\ominus & \verb'\ominus' \\
+\otimes & \verb'\otimes' \\
+\oslash & \verb'\oslash' \\
+\odot & \verb'\odot' \\
+\end{symbols}
+
+\subsubsection{Boxed operators}
+\vspace*{-2.5ex}
+\begin{symbols}[0.2]
+\boxdot & \verb'\boxdot' \\
+\boxplus & \verb'\boxplus' \\
+\boxtimes & \verb'\boxtimes' \\
+\boxminus & \verb'\boxminus' \\
+\end{symbols}
+\subsection{Arrow Symbols}
+\vspace*{-1ex}
+\subsubsection{Left Arrows}
+\vspace*{-2.5ex}
+\begin{symbols}[0.7]
+\leftarrow & \verb'\leftarrow \gets' \\
+\Leftarrow & \verb'\Leftarrow' \\
+\hookleftarrow & \verb'\hookleftarrow' \\
+\leftharpoonup & \verb'\leftharpoonup' \\
+\leftharpoondown & \verb'\leftharpoondown' \\
+\longleftarrow & \verb'\longleftarrow' \\
+\Longleftarrow & \verb'\Longleftarrow' \\
+\twoheadleftarrow & \verb'\twoheadleftarrow' \\
+\leftleftarrows & \verb'\leftleftarrows' \\
+\leftarrowtail & \verb'\leftarrowtail' \\
+\Lleftarrow & \verb'\Lleftarrow' \\
+\nleftarrow & \verb'\nleftarrow' \\
+\nLeftarrow & \verb'\nLeftarrow' \\
+\end{symbols}
+
+\subsubsection{Right Arrows}
+\begin{symbols}[0.7]
+\rightarrow & \verb'\rightarrow \to' \\
+\Rightarrow & \verb'\Rightarrow' \\
+\map & \verb'\map' \\
+\longmapsto & \verb'\longmapsto' \\
+\hookrightarrow & \verb'\hookrightarrow' \\
+\rightharpoonup & \verb'\rightharpoonup' \\
+\rightharpoondown & \verb'\rightharpoondown' \\
+\leadsto & \verb'\leadsto' \\
+\longrightarrow & \verb'\longrightarrow' \\
+\Longrightarrow & \verb'\Longrightarrow' \\
+\twoheadrightarrow & \verb'\twoheadrightarrow' \\
+\rightrightarrows & \verb'\rightrightarrows' \\
+\rightarrowtail & \verb'\rightarrowtail' \\
+\rightsquigarrow & \verb'\rightsquigarrow' \\
+\Rrightarrow & \verb'\Rrightarrow' \\
+\nrightarrow & \verb'\nrightarrow' \\
+\nRightarrow & \verb'\nRightarrow' \\
+\end{symbols}
+
+\subsubsection{Left Right Arrows}
+\begin{symbols}[0.6]
+\leftrightarrow & \verb'\leftrightarrow' \\
+\Leftrightarrow & \verb'\Leftrightarrow' \\
+\rightleftharpoons & \verb'\rightleftharpoons' \\
+\longleftrightarrow & \verb'\longleftrightarrow' \\
+\Longleftrightarrow & \verb'\Longleftrightarrow' \\
+\rightleftharpoons & \verb'\rightleftharpoons' \\
+\leftrightharpoons & \verb'\leftrightharpoons' \\
+\leftrightarrows & \verb'\leftrightarrows' \\
+\rightleftarrows & \verb'\rightleftarrows' \\
+\leftrightsquigarrow & \verb'\leftrightsquigarrow' \\
+\nLeftrightarrow & \verb'\nLeftrightarrow' \\
+\nleftrightarrow & \verb'\nleftrightarrow' \\
+\end{symbols}
+
+\subsubsection{Up Down Arrows}
+\begin{symbols}[1]
+\uparrow & \verb'\uparrow' \\
+\Uparrow & \verb'\Uparrow' \\
+\downarrow & \verb'\downarrow' \\
+\Downarrow & \verb'\Downarrow' \\
+\updownarrow & \verb'\updownarrow' \\
+\Updownarrow & \verb'\Updownarrow' \\
+\upuparrows & \verb'\upuparrows' \\
+\downdownarrows & \verb'\downdownarrows' \\
+\upharpoonright & \verb'\upharpoonright' \\
+\downharpoonright & \verb'\downharpoonright' \\
+\upharpoonleft & \verb'\upharpoonleft' \\
+\downharpoonleft & \verb'\downharpoonleft' \\
+\end{symbols}
+
+\subsubsection{Miscellaneous}
+\begin{symbols}[0.9]
+\nearrow & \verb'\nearrow' \\
+\searrow & \verb'\searrow' \\
+\swarrow & \verb'\swarrow' \\
+\nwarrow & \verb'\nwarrow' \\
+\circlearrowright & \verb'\circlearrowright' \\
+\circlearrowleft & \verb'\circlearrowleft' \\
+\Lsh & \verb'\Lsh' \\
+\Rsh & \verb'\Rsh' \\
+\looparrowleft & \verb'\looparrowleft' \\
+\looparrowright & \verb'\looparrowright' \\
+\curvearrowleft & \verb'\curvearrowleft' \\
+\curvearrowright & \verb'\curvearrowright' \\
+\end{symbols}
+\pagebreak[4]
+
+\subsection{Relations}
+\begin{symbols}[0.8]
+\ll & \verb'\ll' \\
+\gg & \verb'\gg' \\
+\llless & \verb'\lll \llless' \\
+\gggtr & \verb'\ggg \gggtr' \\
+\sqsubset & \verb'\sqsubset' \\
+\sqsupset & \verb'\sqsupset' \\
+\sqsubseteq & \verb'\sqsubseteq' \\
+\sqsupseteq & \verb'\sqsupseteq' \\
+\owns & \verb'\owns' \\
+\vdash & \verb'\vdash' \\
+\Vdash & \verb'\Vdash' \\
+\vDash & \verb'\vDash' \\
+\dashv & \verb'\dashv' \\
+\Vvdash & \verb'\Vvdash' \\
+\models & \verb'\models' \\
+\nvdash & \verb'\nvdash' \\
+\nVdash & \verb'\nVdash' \\
+\nvDash & \verb'\nvDash' \\
+\nVDash & \verb'\nVDash' \\
+\perp & \verb'\perp' \\
+\sim & \verb'\sim' \\
+\simeq & \verb'\simeq' \\
+\eqsim & \verb'\eqsim' \\
+\backsim & \verb'\backsim' \\
+\backsimeq & \verb'\backsimeq' \\
+\thicksim & \verb'\thicksim' \\
+\nsim & \verb'\nsim' \\
+\approx & \verb'\approx' \\
+\napprox & \verb'\napprox' \\
+\thickapprox & \verb'\thickapprox' \\
+\approxeq & \verb'\approxeq' \\
+\asymp & \verb'\asymp' \\
+\cong & \verb'\cong' \\
+\ncong & \verb'\ncong' \\
+\doteq & \verb'\doteq' \\
+\doteqdot & \verb'\Doteq \doteqdot' \\
+\risingdotseq & \verb'\risingdotseq' \\
+\fallingdotseq & \verb'\fallingdotseq' \\
+\lessdot & \verb'\lessdot' \\
+\gtrdot & \verb'\gtrdot' \\
+\eqcirc & \verb'\eqcirc' \\
+\circeq & \verb'\circeq' \\
+\bumpeq & \verb'\bumpeq' \\
+\Bumpeq & \verb'\Bumpeq' \\
+\triangleq & \verb'\triangleq' \\
+\multimap & \verb'\multimap' \\
+\propto & \verb'\propto' \\
+\varpropto & \verb'\varpropto' \\
+\lesssim & \verb'\lesssim' \\
+\gtrsim & \verb'\gtrsim' \\
+\lessapprox & \verb'\lessapprox' \\
+\gtrapprox & \verb'\gtrapprox' \\
+\xprec & \verb'\xprec' \\
+\xsucc & \verb'\xsucc' \\
+\preceq & \verb'\preceq' \\
+\succeq & \verb'\succeq' \\
+\precsim & \verb'\precsim' \\
+\succsim & \verb'\succsim' \\
+\precapprox & \verb'\precapprox' \\
+\succapprox & \verb'\succapprox' \\
+\eqslantless & \verb'\eqslantless' \\
+\eqslantgtr & \verb'\eqslantgtr' \\
+\curlyeqprec & \verb'\curlyeqprec' \\
+\curlyeqsucc & \verb'\curlyeqsucc' \\
+\preccurlyeq & \verb'\preccurlyeq' \\
+\succcurlyeq & \verb'\succcurlyeq' \\
+\leqq & \verb'\leqq' \\
+\geqq & \verb'\geqq' \\
+\leqslant & \verb'\leqslant' \\
+\geqslant & \verb'\geqslant' \\
+\lessgtr & \verb'\lessgtr' \\
+\gtrless & \verb'\gtrless' \\
+\lesseqgtr & \verb'\lesseqgtr' \\
+\Also
+\gtreqless & \verb'\gtreqless' \\
+\Also
+\lesseqqgtr & \verb'\lesseqqgtr' \\
+\Also
+\gtreqqless & \verb'\gtreqqless' \\
+\also
+\lvertneqq & \verb'\lvertneqq' \\
+\gvertneqq & \verb'\gvertneqq' \\
+\nleq & \verb'\nleq' \\
+\ngeq & \verb'\ngeq' \\
+\nless & \verb'\nless' \\
+\ngtr & \verb'\ngtr' \\
+\nprec & \verb'\nprec' \\
+\nsucc & \verb'\nsucc' \\
+\lneqq & \verb'\lneqq' \\
+\gneqq & \verb'\gneqq' \\
+\nleqslant & \verb'\nleqslant' \\
+\ngeqslant & \verb'\ngeqslant' \\
+\lneq & \verb'\lneq' \\
+\gneq & \verb'\gneq' \\
+\npreceq & \verb'\npreceq' \\
+\nsucceq & \verb'\nsucceq' \\
+\precnsim & \verb'\precnsim' \\
+\succnsim & \verb'\succnsim' \\
+\lnsim & \verb'\lnsim' \\
+\gnsim & \verb'\gnsim' \\
+\nleqq & \verb'\nleqq' \\
+\ngeqq & \verb'\ngeqq' \\
+\precneqq & \verb'\precneqq' \\
+\succneqq & \verb'\succneqq' \\
+\precnapprox & \verb'\precnapprox' \\
+\succnapprox & \verb'\succnapprox' \\
+\lnapprox & \verb'\lnapprox' \\
+\gnapprox & \verb'\gnapprox' \\
+\Subset & \verb'\Subset' \\
+\Supset & \verb'\Supset' \\
+\subseteqq & \verb'\subseteqq' \\
+\supseteqq & \verb'\supseteqq' \\
+%\varsubsetneq & \verb'\varsubsetneq' \\
+%\varsupsetneq & \verb'\varsupsetneq' \\
+\nsubseteqq & \verb'\nsubseteqq' \\
+\also
+\nsupseteqq & \verb'\nsupseteqq' \\
+\also
+\subsetneqq & \verb'\subsetneqq' \\
+\also
+\supsetneqq & \verb'\supsetneqq' \\
+%\varsubsetneqq & \verb'\varsubsetneqq' \\
+%\varsupsetneqq & \verb'\varsupsetneqq' \\
+\subsetneq & \verb'\subsetneq' \\
+\supsetneq & \verb'\supsetneq' \\
+\nsubseteq & \verb'\nsubseteq' \\
+\nsupseteq & \verb'\nsupseteq' \\
+\trianglerighteq & \verb'\trianglerighteq' \\
+\trianglelefteq & \verb'\trianglelefteq' \\
+\ntrianglerighteq & \verb'\ntrianglerighteq' \\
+\ntrianglelefteq & \verb'\ntrianglelefteq' \\
+\ntriangleleft & \verb'\ntriangleleft' \\
+\ntriangleright & \verb'\ntriangleright' \\
+\between & \verb'\between' \\
+| & \verb'| \vert \mid' \\
+\| & \verb'\| \Vert \parallel' \\
+\interleave & \verb'\interleave' \\
+\shortmid & \verb'\shortmid' \\
+\shortparallel & \verb'\shortparallel' \\
+\shortinterleave & \verb'\shortinterleave' \\
+\nparallel & \verb'\nparallel' \\
+\nmid & \verb'\nmid' \\
+\nshortmid & \verb'\nshortmid' \\
+\nshortparallel & \verb'\nshortparallel' \\
+\end{symbols}
+
+\subsection{Binary Operations}
+\begin{symbols}[1.4]
+\curlywedge & \verb'\curlywedge' \\
+\curlyvee & \verb'\curlyvee' \\
+\veebar & \verb'\veebar' \\
+\barwedge & \verb'\barwedge' \\
+\doublebarwedge & \verb'\doublebarwedge' \\
+\pm & \verb'\pm' \\
+\mp & \verb'\mp' \\
+\times & \verb'\times' \\
+\ltimes & \verb'\ltimes' \\
+\rtimes & \verb'\rtimes' \\
+\leftthreetimes & \verb'\leftthreetimes' \\
+\rightthreetimes & \verb'\rightthreetimes' \\
+\divideontimes & \verb'\divideontimes' \\
+\divides & \verb'\divides' \\
+\uplus & \verb'\uplus' \\
+\sqcap & \verb'\sqcap' \\
+\sqcup & \verb'\sqcup' \\
+\Cup & \verb'\Cup \doublecup' \\
+\Cap & \verb'\Cap \doublecap' \\
+\backslash & \verb'\backslash' \\
+\setminus & \verb'\setminus' \\
+\smallsetminus & \verb'\smallsetminus' \\
+\wr & \verb'\wr' \\
+\lhd & \verb'\lhd' \\
+\rhd & \verb'\rhd' \\
+\unlhd & \verb'\unlhd' \\
+\unrhd & \verb'\unrhd' \\
+\restriction & \verb'\restriction' \\
+\amalg & \verb'\amalg' \\
+\top & \verb'\top' \\
+\bot & \verb'\bot' \\
+\smallsmile & \verb'\smallsmile' \\
+\smallfrown & \verb'\smallfrown' \\
+\smile & \verb'\smile' \\
+\frown & \verb'\frown' \\
+\pitchfork & \verb'\pitchfork' \\
+\dotplus & \verb'\dotplus' \\
+\Join & \verb'\Join' \\
+\bowtie & \verb'\bowtie' \\
+\end{symbols}
+
+\subsection{Miscellaneous Symbols}
+\begin{symbols}
+\dagger & \verb'\dagger' \\
+\ddagger & \verb'\ddagger' \\
+\sectionsymbol & \verb'\sectionsymbol' \\
+\P & \verb'\P' \\
+\angle & \verb'\angle' \\
+\measuredangle & \verb'\measuredangle' \\
+\sphericalangle & \verb'\sphericalangle' \\
+\prime & \verb'\prime' \\
+\backprime & \verb'\backprime' \\
+\surd & \verb'\surd' \\
+\smallint & \verb'\smallint' \\
+\flat & \verb'\flat' \\
+\natural & \verb'\natural' \\
+\sharp & \verb'\sharp' \\
+\partial & \verb'\partial' \\
+\infty & \verb'\infty' \\
+\yen & \verb'\yen' \\
+\therefore & \verb'\therefore' \\
+\because & \verb'\because' \\
+\checkmark & \verb'\checkmark' \\
+\end{symbols}
+
+\subsection{Variable-sized Symbols}
+These symbols come in two sizes which
+do not vary with the point size of your
+font. The big size can be obtained
+by preceding the symbol command with
+the command \verb'\displaystyle'.
+\begin{symbols}[1.3]
+\sum \displaystyle \sum & \verb'\sum' \\
+\product \displaystyle \product & \verb'\product' \\
+\coprod \displaystyle \coprod & \verb'\coprod' \\
+\integral \displaystyle \integral & \verb'\integral' \\
+\oint \displaystyle \oint & \verb'\oint' \\
+\bigcap \displaystyle \bigcap & \verb'\bigcap' \\
+\bigcup \displaystyle \bigcup & \verb'\bigcup' \\
+\bigsqcup \displaystyle \bigsqcup & \verb'\bigsqcup' \\
+\bigvee \displaystyle \bigvee & \verb'\bigvee' \\
+\bigwedge \displaystyle \bigwedge & \verb'\bigwedge' \\
+\bigodot \displaystyle \bigodot & \verb'\bigodot' \\
+\bigotimes \displaystyle \bigotimes & \verb'\bigotimes' \\
+\bigoplus \displaystyle \bigoplus & \verb'\bigoplus' \\
+\biguplus \displaystyle \biguplus & \verb'\biguplus' \\
+\end{symbols}
+
+\subsection{Delimiters}
+\vspace*{-1ex}
+These symbols can be made large to surround large formula.
+E.g., $$\left\lfloor\displaystyle\sum_{i=1}^n x^i\right\rfloor$$
+was generated using
+
+\begin{verbatim}
+\left\lfloor...\right\rfloor
+\end{verbatim}
+\vspace*{-2ex}
+\begin{symbols}[0.8]
+(~~~) & \verb'( )' \\
+\{~~~\} & \verb'\{ \}' \\
+\lfloor~~~\rfloor & \verb'\lfloor \rfloor' \\
+\lceil~~~\rceil & \verb'\lceil \rceil' \\
+\langle~~~\rangle & \verb'\langle \rangle' \\
+\ulcorner~~~\urcorner & \verb'\ulcorner \urcorner' \\
+\llcorner~~~\lrcorner & \verb'\llcorner \lrcorner' \\
+\uparrow & \verb'\uparrow' \\
+\downarrow & \verb'\downarrow' \\
+\updownarrow & \verb'\updownarrow' \\
+\Uparrow & \verb'\Uparrow' \\
+\Downarrow & \verb'\Downarrow' \\
+\Updownarrow & \verb'\Updownarrow' \\
+\end{symbols}
+
+\subsection{Math Accents}
+\vspace*{-1ex}
+\begin{symbols}[0.2]
+\hat{a} & \verb'\hat{a}' \\
+\widehat{a} & \verb'\widehat{a}' \\
+\widehat{aa} & \verb'\widehat{aa}' \\
+\widehat{aaa} & \verb'\widehat{aaa}' \\
+\tilde{a} & \verb'\tilde{a}' \\
+\widetilde{a} & \verb'\widetilde{a}' \\
+\widetilde{aa} & \verb'\widetilde{aa}' \\
+\widetilde{aaa} & \verb'\widetilde{aaa}' \\
+\check{a} & \verb'\check{a}' \\
+\breve{a} & \verb'\breve{a}' \\
+\acute{a} & \verb'\acute{a}' \\
+\grave{a} & \verb'\grave{a}' \\
+\bar{a} & \verb'\bar{a}' \\
+\vec{a} & \verb'\vec{a}' \\
+\dotaccent{a} & \verb'\dotaccent{a}' \\
+\ddot{a} & \verb'\ddot{a}' \\
+\end{symbols}
+
+\subsection{Size Commands}
+\vspace*{-1ex}
+\begin{symbols}
+\mu~\zsmall\mu~\zSmall\mu &\verb'\mu \zsmall\mu \zSmall\mu'\\
+\zbig\mu~\zBig\mu~\zBIG\mu &\verb'\zbig\mu \zBig\mu \zBIG\mu'\\
+\end{symbols}
+\end{multicols}
+\end{document}
diff --git a/macros/latex/contrib/objectz/oztest.tex b/macros/latex/contrib/objectz/oztest.tex
new file mode 100644
index 0000000000..fc8ea11c93
--- /dev/null
+++ b/macros/latex/contrib/objectz/oztest.tex
@@ -0,0 +1,206 @@
+\documentclass[11pt]{article}
+\usepackage{oz}
+\def\Out#1{#1 \!\!\rightarrow}
+\def\In#1{\rightarrow\!\! #1}
+\begin{document}
+
+Multi-letter identifiers have been changed to look
+better than they do with vanilla \LaTeX: instead of
+$\mathit{specifications}$, you get $specifications$.
+The letters haven't been spread apart, and the
+ligature $fi$ has been used.
+
+{\tt This is in typewriter font}
+
+
+\begin{schema}{BirthdayBook}
+ known: \pset NAME \\
+ birthday: NAME \pfun DATE
+\ST
+ known = \dom birthday
+\end{schema}
+
+\begin{axdef}
+limit : \nat
+\ST
+limit \leq 65536
+\end{axdef}
+
+\begin{class}{Shape}
+\also
+colour : Colour \\
+\end{class}
+
+\begin{axdef}
+perim : \real
+\ST
+perim > 0
+\end{axdef}
+
+\begin{axdef}
+ini:State \cross Occ \cross T \fun Bool
+\where
+\forall S:State, i: Occ, t:T \dot ini(S,i,t) \iff \\
+\t1 \theta(\Out{S}, 1,0)\land\\
+\t2 \exi t_{1}:T \dot \theta(\In{S},i,t_{1}) \land
+t_{1}\leq t \land \forall t_{2}:T \dot t_{2} < t \imp \neg \theta(\Out{S},i+1,t_{2}
+)\\
+\t1 \lor \theta(\In{S}, 1,0)\land\\
+\t2 \exi t_{1}:T \dot \theta(\In{S},i,t_{1}) \land
+t_{1}\leq t \land \forall t_{2}:T \dot t_{2} < t \imp \neg
+\theta(\Out{S},i,t_{2})
+\end{axdef}
+
+Let us see if \verb|zbreak| works:
+\typeout{*************************************}
+\typeout{If you get large overfull vboxes now, Oz is not working}
+\typeout{*************************************}
+
+\def \comm{\comment}
+
+\begin{schema}{MakePlan}
+ c? : Company \comm{The company that is making the plan}\\
+ t? : Month \comm{Time period} \\
+ \Xi NFMM \\
+ \Xi AttrOfMarkets \comm{OpenMarkets} \\
+ \Xi Cost \\
+ \Xi AttrOfEconomy \comm{Buying and selling price of quota }\\
+ \Xi AttrOfQuota \\
+ \Xi AttrOfProduction \\
+ \Xi FishingLimitations \\
+ Plans! : Company \fun Plan \comm{The output is the plan for
+ the company} \\
+\zbreak
+\where
+ \forall v: Vessel; f: Fishery; s: QuotaStock; p: Product; \\
+\t0 l: Landing; t: Month; i: Input @ \\
+\t0 \exists plan: Plan; Months: \power Month; \\
+\t0 vs : \power Vessel; fs: \power Fishery ; qs: \power QuotaStock; ls: \power Landing; \\
+\t0 ps : \power Product; \\
+\t0 catch: Vessel \cross Fishery \cross QuotaStock \pfun Tons; \\
+\t0 MAXnet\_profit:Kronur; fishing\_cost:Kronur; \\
+ \t1 production\_earnings:Kronur; \\
+ \t1 production\_cost:Kronur; quota\_trading\_profit:Kronur; \\
+\t0 fishing\_days: Vessel \cross Fishery \cross Month \pfun \nat; \\
+\t0 value\_landing: Vessel \fun Kronur; \\
+\t0 export: Vessel \cross Landing \cross Month \pfun Tons; \\
+ \t1 trade\_in, trade\_out: Landing \cross Month \pfun Tons; \\
+ \t1 prod: Product \cross Month \fun Tons; \\
+\t0 quota\_rent\_in, quota\_rent\_out, quota\_next\_to, \\
+ \t1 quota\_next\_from, quota\_exch\_to, quota\_exch\_from,\\
+ \t1 quota\_trans\_from, quota\_trans\_to: Vessel \cross QuotaStock \pfun Tons; \\
+\t0 ExchangeCharge: \num; \comm{charge for changing one species into another} \\
+\t0 quota\_used: Vessel \cross QuotaStock \pfun Tons @ \\
+\zbreak
+ \t0 Plans! = Plans! \oplus \{c? \mapsto plan \} \land \\
+ \t0 Months = t? \upto 12 \land \\
+ \t0 i \in Inputs \land \\
+ \t0 vs = Vessels ~ c? \land v \in vs \land\\
+ \t0 fs = \{f: Fishery | f \in \\
+ \t1 (\bigcup \{ v: Vessel | v \in vs @ Fisheries(v) \}) @ f \} \land f \in fs \land \\
+ \t0 qs = \{s: QuotaStock; f: Fishery | \\
+ \t1 f \in fs \land s \in QuotaStocks (f) @ s \} \land s \in qs \land \\
+ \t0 ls = \{s: QuotaStock; f: Fishery | f \in fs \land s \in qs @ \\
+ \t1 Landings~(f,s) \} \land l \in ls \land \\
+ \t0 ps = \{p: Product | \\
+ \t1 p \in \bigcup \{ fa: Factory | fa \in Factories~c? @ Products(fa) \} @ p \} \land \\
+ \t0 p \in ps \land \\
+\comm{The overall goal is to maximize net profits} \\
+ \t0 MAXnet\_profit = -fishing\_cost+production\_earnings + \\
+ \t1 -production\_cost + quota\_trading\_profit \land \comm{A.1}\\
+ \t0 catch ~(v,f,s) = ExpCatch~(v,f,s)* \comm{A.4}\\
+ \t1 \sum_{t: Month | t \in Months} fishing\_days~(v,f,t) \land \\
+\comm{One of the prices LandingPrice or ExportPrice is always zero for any l} \\
+ \t0 (\forall l | l \in ls @ LandingPrice (l) = 0 \lor ExportPrice(l) = 0 \land \\
+ \t1 LandingPrice(l) \neq ExportPrice(l) ) \land \\
+ \t0 value\_landing= \comm{A.3} \\
+ \t1 \{v: Vessel | v \in vs @ v \mapsto \\
+ \t1 \sum_{ l: Landing | l \in ls} LandingPrice (l)* ExportPriceConst(l) * \\
+ \t1 \sum_{f: Fishery | f \in fs} \sum_{s: QuotaStock | s \in qs} (SpeciesToLandings~(s,f,l) *(catch~(v,f,s)) \}\land \\
+ \t0 fishing\_cost = \sum_{v: Vessel | v \in vs} Share (v)*value\_landing(v) + \comm{A.2}\\
+ \t1 \sum_{ f: Fishery | f \in fs} CostFishDay ~ (v, f) * \\
+ \t1 \sum_{t: Month | t \in Months} fishing\_days~(v,f,t) \land \\
+\zbreak
+ \t0 production\_earnings = \comm{A.5}\\
+ \t1 \sum_{l: Landing | l \in ls} \sum_{ t: Month | t \in Months} \\
+ \t3 (ExportPrice~(l,t))*(1-0.002)*t)* \\
+ \t3 \sum_{v: Vessel | v \in vs} export~(v,l,t) \\
+ \t1 -WetfishBuyingPrice(l) * (1-0.002)*t)*trade\_in~(l,t) \\
+ \t1 +WetfishSellingPrice(l) * (1-0.002)*t)*trade\_out~(l,t) \\
+ \t1 +\sum_{p: Product | p \in ps} ProductPrice~(p,t) *(1-0.002)*t)* \\
+ \t1 \sum_{t:Month | t \in Months} prod~ (p,t) \land \\
+ \t0 production\_cost = \sum_{i: Input | i \in Inputs} InputCost(i)* \comm{A.6}\\
+ \t1 \sum_{p: Product | p \in ps} InputForProduct(p,i) * \\
+ \t1 \sum_{ t: Month | t \in Months} prod(p,t) \land \\
+ \t0 ExchangeCharge = 0.005*NextPrice(s) \land \\
+ \t0 quota\_trading\_profit = -(\sum_{s: QuotaStock | s \in qs } QuotaRentInPrice(s) * \\
+ \t1 \sum_{v: Vessel | v \in vs } quota\_rent\_in~(v,s) ) \comm{A.7}\\
+ \t1 + \sum_{s: QuotaStock | s \in qs } QuotaRentOutPrice(s)* \\
+ \t1 \sum_{v: Vessel | v \in vs } quota\_rent\_out~(v,s) \\
+ \t1 + \sum_{s: QuotaStock | s \in qs } NextCharge *NextPrice(s)*(1-InterestRate)* \\
+ \t1 \sum_{v: Vessel | v \in vs } quota\_next\_to~(v,s) \\
+ \t1 + \sum_{s: QuotaStock | s \in qs } NextPrice(s)*(1-InterestRate) * \\
+ \t1 \sum_{v: Vessel | v \in vs } quota\_next\_from~(v,s) \\
+ \t1 -ExchangeCharge*\sum_{v: Vessel | v \in vs }\sum_{s: QuotaStock | s \in qs } quota\_exch\_to(v,s) \\
+ \t1 -TransferCharge*\sum_{v: Vessel | v \in vs }\sum_{s: QuotaStock | s \in qs } quota\_trans\_to~(v,s) \land \\
+ \t0 \sum_{ f: Fishery | f \in fs } fishing\_days~(v,f,t) \leq MaxTotFishingDays ~(v,t) \land \comm{A.9}\\
+\comm{A.6.1 Constraints on fishing time } \\
+ \t0 l \in ExportLandings \implies \\
+ \t1 \sum_{f: Fishery | f \in fs } \sum_{s: QuotaStock | s \in qs } \comm{A.10} \\
+ \t2 SpeciesToLandings~(s,f,l) * ExpCatch (v,f,s)*fishing\_days(v,f,t) = \\
+ \t3 export~(v,l,t) \land \\
+\comm{A.6.2 Processing and selling the catch } \\
+ \t0 l \notin ExportLandings \implies \\
+ \t1 \sum_{v: Vessel | v \in vs } \sum_{f: Fishery | f \in fs } \sum_{s: QuotaStock | s \in qs } \\
+ \t2 SpeciesToLandings~(s,f,l)*ExpCatch~(v,f,s)*fishing\_days~(v,f,t) \\
+ \t1 = (1 / LandingsToProducts~(p,l)) * prod~(p,t) - trade\_in~(l,t) + trade\_out(l,t) \land \comm{A.11}\\
+\zbreak
+ \t0 \sum_{t: Month | t \in Months } \sum_{p:Product | p \in ps }InputForProduct(p,i)*prod(p,t) \\
+ \t1 \leq \sum_{i : Input | i \in Inputs } MaxInput~(i,t) \land \comm{A.13}\\
+ \t0 \sum_{t: Month | t \in Months } \sum_{p: Product | p \in ps } InputForProduct(p,i)*prod~(p,t) \\
+ \t1 \geq \sum_{i: Input | i \in Inputs } MinInput~(i,t) \land \comm{A.14}\\
+ \t0 \sum_{t: Month | t \in Months } export~(v,l,t) \leq MaxExport~(v,l) \land \comm{A.15}\\
+\comm{A.6.3 Constraints because of quota restrictions } \\
+ \t0 quota\_used = \comm{A.17} \\
+ \t1 \{ v:Vessel; s: QuotaStock | v \in vs \land s \in qs @ \\
+ \t2 (v,s) \mapsto \sum_{f: Fishery | f \in fs } (1+QuotaSurcharge~(s,f))* \\
+ \t2 catch~(v,f,s) \} \land \\
+ \t0 \sum_{v: Vessel | v \in vs } quota\_trans\_to(v,s)- quota\_trans\_from(v,s) =0 \land \comm{A.18} \\
+ \t0 quota\_used(v,s) - quota\_rent\_in(v,s) + quota\_rent\_out(v,s) - \comm{A.16} \\
+ \t1 quota\_exch\_to(v,s) + quota\_exch\_from(v,s) - \\
+ \t1 quota\_trans\_to(v,s) + quota\_trans\_from(v,s) - \\
+ \t1 quota\_next\_to~(v,s) + quota\_next\_from~(v,s) \leq QuotaLeft~(v,s) \land \\
+ \t0 s = Cod \implies MaxQuotaInto(v,s) = 0 \land \comm{A.19}\\
+ \t0 s \neq Cod \implies MaxQuotaInto(v,s) = 0.05*QuotaAllocated(v,s) \land \\
+ \t1 QuotaValueInto(s)*quota\_exch\_to(v,s) \leq \\
+ \t2 \sum_{s: QuotaStock | s \in qs } MaxQuotaInto~(v,s) \land \\
+ \t0 \sum_{s: QuotaStock | s \in qs } QuotaValueInto (s)*quota\_exch\_to~(v,s) - \comm{A.20}\\
+ \t1 \sum_{s: QuotaStock | s \in qs } QuotaValueFrom(s)* quota\_exch\_from~(v,s) = 0 \land \\
+ \t0 quota\_next\_from(v,s) \leq (QuotaOver(v,s) / 100)*QuotaAllocated(v,s) \land \comm{A.21}\\
+ \t0 quota\_next\_to~(v,s) \leq (QuotaUnder(v,s) / 100)*QuotaAllocated(v,s) \land \comm{A.22} \\
+\zbreak
+\comm{Bounds} \\
+ \t0 fishing\_days~(v,f,t) \leq MaxFishingDays~(f,t) \land \comm{A.23}\\
+ \t0 QuotaAllocated~(v,s) = 0 \implies \\
+ \t1 (quota\_exch\_to~(v,s) = 0 \land \comm{A.24}\\
+ \t1 quota\_rent\_in~(v,s) = 0 \land \comm{A.25}\\
+ \t1 quota\_trans\_to~(v,s) = 0) \land \comm{A.26} \\
+ \t0 QuotaValueInto~s = 0 \implies quota\_exch\_to~(v,s) = 0 \land \comm{A.27}\\
+ \t0 QuotaValueFrom~s = 0 \implies quota\_exch\_from~(v,s) = 0 \comm{A.28}\\
+\zbreak
+ \t0 plan.c = c? \
+ \t0 plan.fishing\_days = fishing\_days \land
+ \t0 plan.quota\_rent\_out = quota\_rent\_out \land \\
+ \t0 plan.quota\_rent\_in = quota\_rent\_in \land \\
+ \t0 plan.quota\_trans\_from = quota\_trans\_from \land \\
+ \t0 plan.quota\_trans\_to = quota\_trans\_to \land \\
+ \t0 plan.quota\_next\_from = quota\_next\_from \land \\
+ \t0 plan.quota\_next\_to = quota\_next\_to \land \\
+ \t0 plan.quota\_exch\_from = quota\_exch\_from \land \\
+ \t0 plan.quota\_exch\_to = quota\_exch\_to \land \\
+ \t0 plan.trade\_out = trade\_out \land \\
+ \t0 plan.trade\_in = trade\_in \land \\
+ \t0 plan.prod = prod \land \\
+ \t0 plan.export = export \\
+\end{schema}
+\end{document}
diff --git a/macros/latex/contrib/objectz/readme b/macros/latex/contrib/objectz/readme
new file mode 100644
index 0000000000..c3ee8cd92f
--- /dev/null
+++ b/macros/latex/contrib/objectz/readme
@@ -0,0 +1,45 @@
+This is a revision of Paul King's oz.sty macros for typesetting Object Z,
+updated for LaTeX2e. Users should run ozguide.tex through \LaTeX\ (after
+installation!) for details of usage.
+
+Install by running \TeX\ on oz.ins and install oz.sty where \LaTeX\
+can find it.
+
+UPDATE NOVEMBER 1996
+********************
+
+The Formal Methods Group in the Computer Science Department at the
+University of Queensland recently released 'wizard', a type checker
+for Object-Z specifications. Included in the wizard release was an
+updated version of the oz.sty file for LaTeX 2.09.
+
+I have implemented all changes made in the oz.sty for LaTeX 2.09,
+since it's last official release in late 1990, into the oz.dtx file
+which you maintain for LaTeX 2e. I have attached my updated version
+of oz.dtx to this message so that you may check these modifications
+and officially release the updated version.
+
+The changes were made to the oz.dtx file with last changes logged
+on 22 Feb 95 (this is the version currently available from CTAN).
+All modifications and additions I have made are clearly indicated in
+the updated file for your convenience.
+
+Should you need to compare my changes with the updated oz.sty file for
+LaTeX 2.09, you can download the wizard archive from the following url:
+
+ ftp://ftp.cs.uq.edu.au/pub/SVRC/software/wizard.tar.gz
+
+The new oz.sty file and oz.tex file are located in the wizard/tex
+subdirectory when the archive is extracted.
+
+Please contact me if you need to.
+
+Thanks.
+
+Dave.
+--
+David Leadbetter Email: davidl@cs.uq.edu.au
+PhD Student Phone: + 61 7 3365 1204
+Department of Computer Science FAX: + 61 7 3365 1999
+The University Of Queensland 4072 AUSTRALIA
+