% \iffalse meta-comment
%
% Sebastian Rahtz, 7.93. spqr@minster.york.ac.uk
%
% This file is designed to be
% used with the NFSS (New Font Selection Scheme) package.
% 
% \fi
\def\fileversion{4.1}
\def\filedate{11.07.93}
% \title{The {\tt psstyles.doc} file\thanks
%         {This file has version number \fileversion, dated \filedate}.
%       for use with the new font selection scheme}
% \author{Sebastian Rahtz}
%
% \maketitle
%
%
% \StopEventually{}
%
% As always we begin by identifying the latest version of this file
% on the VDU and in the {\sf log} file.
%    \begin{macrocode}
%<*main>
\newlinechar`\^^J
\immediate\write\sixt@@n{File: `psstyles'  \space
 \fileversion\space <\filedate> (SPQR)}
\immediate\write\sixt@@n
  {********************************************************************}
%</main>
%<*style>
%  For the style file we have to make sure that it runs under NFSS
% release 2, so we check for appropriate command names.
%    \begin{macrocode}
\@ifundefined{DeclareFontShape}
     {\@ifundefined{selectfont}
        {\@latexerr{This style option can only be used
                    with the new^^Jfont selection scheme}\@eha}
        {\@latexerr{This style option can only be used
                    with the new^^Jfont selection scheme *release 2*}
                   {Your format contains NFSS release 1, but this style
                    option was^^Jdeveloped for release 2.}
        }
      \endinput}
     {}
\immediate\write\sixt@@n{PSNFSS2 \fileversion\space <\filedate> (SPQR)}
%</style>
%<*nfmtimes>
\immediate\write\sixt@@n{File: `nfmtimes.sty' }
\renewcommand{\sfdefault}{pun}
\renewcommand{\rmdefault}{mnt}
\renewcommand{\ttdefault}[T1]{cmtt}
\def\bfdefault{b}
%</nfmtimes>
%<*nfimpri>
\immediate\write\sixt@@n{File: `nfimpri.sty' }
\renewcommand{\sfdefault}{mim}
\renewcommand{\rmdefault}{pgs}
\renewcommand{\ttdefault}{pcr}
\def\bfdefault{b}
%</nfimpri>
%<*nfbembo>
\immediate\write\sixt@@n{File: `nfbembo.sty' }
\renewcommand{\sfdefault}{pop}
\renewcommand{\rmdefault}{pbe}
\renewcommand{\ttdefault}{pcr}
\def\bfdefault{b}
%</nfbembo>
%<*nfgaram>
\immediate\write\sixt@@n{File: `nfgaram.sty' }
\renewcommand{\sfdefault}{pop}
\renewcommand{\rmdefault}{pgm}
\renewcommand{\ttdefault}{pcr}
\def\bfdefault{b}
%</nfgaram>
%<*nfbaske>
\immediate\write\sixt@@n{File: `nfbaske.sty' }
\renewcommand{\sfdefault}{pun}
\renewcommand{\rmdefault}{pnb}
\renewcommand{\ttdefault}{pcr}
\def\bfdefault{b}
%</nfbaske>
%<*nflucid>
\immediate\write\sixt@@n{File: `nflucid.sty' }
\renewcommand{\sfdefault}{plcs}
\renewcommand{\rmdefault}{plc}
\renewcommand{\ttdefault}{pcr}
\def\bfdefault{b}
%</nflucid>
%<*nflucma>
\immediate\write\sixt@@n{File: `nflucma.sty' }
%
\DeclareSymbolFont{operators}{\encodingdefault}{\rmdefault}{m}{n}
\DeclareSymbolFont{letters}{OML}{plcm}{m}{it}
\DeclareSymbolFont{symbols}{OMS}{plcm}{m}{n}
\DeclareSymbolFont{largesymbols}{OMX}{plcm}{m}{n}
\DeclareSymbolFont{italics}{\encodingdefault}{\rmdefault}{m}{it}
%
\SetSymbolFont{letters}{bold}{OML}{plcm}{m}{it}%
\SetSymbolFont{operators}{bold}{\encodingdefault}{\rmdefault}{b}{n}%
\SetSymbolFont{operators}{normal}{\encodingdefault}{\rmdefault}{m}{n}%
\SetMathAlphabet{\mathbf}{normal}{\encodingdefault}{\rmdefault}{b}{n}%
\SetMathAlphabet{\mathsf}{normal}{\encodingdefault}{\sfdefault}{m}{n}%
\SetMathAlphabet{\mathrm}{normal}{\encodingdefault}{\rmdefault}{m}{n}%
\SetMathAlphabet{\mathbf}{bold}{\encodingdefault}{\rmdefault}{m}{n}%
\SetMathAlphabet{\mathsf}{bold}{\encodingdefault}{\sfdefault}{b}{n}%
\SetMathAlphabet{\mathrm}{bold}{\encodingdefault}{\rmdefault}{b}{n}%
%
%</nflucma>
%<*nfoz>
%
%
\def\filename{nfoz.sty}
%
\typeout{<Style option \filename, \filedate>}
%
%	This document is organised as follows:
%
%	SECTION 1	Z FONTS
%	SECTION 2	Z SYMBOLS
%	SECTION 3	Z ENVIRONMENTS
%
% Modification History:
%
%               The original zed.sty file was written by Mike Spivey.
%               These macros have been extensively modified to
%               include extra symbols and environments for Object-Z
%               and now have little resemblence to the original macros.
%               Mike Spivey has also extended his macros along
%               different lines for Z - the latest version of macros
%               are called fuzz.sty and come with a syntax checker for Z.
%               They can be purchased for a small fee from:
%                       mike@prg.oxford.ac.uk
%
%        87	original zed.sty file - Mike Spivey
%        88	modified to include extra symbols and environments - Paul King
%        88	modified to include macros for UQ editor - Ray Neucom
%    May 89	modified to include object-oriented constructs - PK
%    Jun 89	modified to automatically change Z symbol size - PK
% 27 Jul 89	removed spurious space from \@setsize - PK
%  3 Aug 89	adjust style of equation number field - PK
% 24 Aug 89     add optional field to topline and zedline for proofs - PK
% 15 Sep 89     added extra qed symbols, updated classcom and comment - PK
% 25 Sep 89	renamed z@[bB]ig to z[bB]ig and changed temporal symbols - PK
% 30 Sep 89	added \znewpage, \Infrule, removed space above state box - PK
% 12 Mar 90	changed \@setsize to work better for double-spaced text - PK
% 31 Mar 90	added definition for @ and \bool and redefined `;' - PK
%  9 May 90	changed \sdef to \varsdef, \sdef & \defs to Spivey's latest - PK
% 27 May 90	added \c{n}{text} - a tab like \t{n} with text at left - PK
% 29 May 90	added `corners' to boxes and \zedcornerheight - PK
% 11 Jul 90	added \rename*[y/x] and \zseq \zset ..., changed \zeq \zimp - PK
%  2 Aug 90     added subseq - PK
%  9 Nov 90	changed \M to hopefully interact better with spacing -  PK
% 24 Feb 92     changed to work with NFSS - Sebastian Rahtz
%               check out \@ifundefined at start to isolate
%               differences
% 29 Dec 92     changed to work with NFSS2 - Sebastian Rahtz
%               REMOVED the old code. This is NFSS2 only!!!
%
% Please post any updates that you may make to this file to:
%	Paul King -- ACSnet: king@batserver.cs.uq.oz.au
%---------------------------
%
%	SECTION 1	Z FONTS
%
% The AMS extra symbol fonts are loaded.
%	Note: 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)
%
\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{\bbold}{AMSb}
\mathversion{oz}
%
% 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
%
\newbox\strutbox@
\def\strut@{\copy\strutbox@}
\addto@hook\every@size{%
    \setbox\strutbox@\hbox{\lower.5\normallineskiplimit
         \vbox{\kern-\normallineskiplimit\copy\strutbox}}}
\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@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}}
%
%	WORD STYLES
% these need handling a bit differently in NFSS
%
\def\String#1{\hbox{`{\tt #1}'}}
\def\STRING#1{\hbox{``{\tt #1}''}}
\def\infix#1{\z@rel{{\underline{#1}}}}
\def\word#1{\z@op{#1}}
\def\keyword#1{\z@op{\mbox{\mathrm{#1}}}}
\def\boldword#1{\z@op{\mbox{\mathbf{#1}}}}
\def\underword#1{\z@op{{\underline{#1}}}}
\def\underkeyword#1{\z@op{{\underline{\mbox{\mathrm{#1}}}}}}
\def\underboldword#1{\z@op{{\underline{\mbox{\mathbf{#1}}}}}}

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

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

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

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

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

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

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

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

% \p and \f make arrows with 1 and 2 crossings resp.
\def\p#1{\mathrel{\ooalign{\hfil$\mapstochar\mkern 5mu$\hfil\cr$#1$}}}
\def\f#1{\mathrel{\ooalign{\hfil
	$\mapstochar\mkern 3mu\mapstochar\mkern 5mu$\hfil\cr$#1$}}}
%
%	------ AMSTEX SYMBOL DEFINITIONS ------
%
% do these before Z symbols so that we can use them in our special symbols
%
%	msam font
%
% AMSa font
\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}
\let\restriction\upharpoonright
\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}
\let\Doteq\doteqdot
\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}
\let\doublecup\Cup
\DeclareMathSymbol\Cap{\mathbin}{AMSa}{"65}
\let\doublecap\Cap
\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}
\let\llless\lll
\DeclareMathSymbol\ggg{\mathrel}{AMSa}{"6F}
\let\gggtr\ggg

\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}
%
%AMSb font
%
\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}
\def\napprox{\not\approx}
%\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}
\def\interleave{{\parallel\!\!\vert}}
\def\shortinterleave{\z@rel{\mathord\shortmid\mathord\shortparallel}}
\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}
%
%		------ SPECIAL Z SYMBOLS ------
%
%	NUMBERS
%
\def \nat	{{\bbold N}}
\def \integer	{{\bbold Z}}
\def \natone	{{\bbold N}_1}
\def \real	{{\bbold R}}
\def \bool	{{\bbold B}}
\let \divides	\div
\def \div	{\z@bin{\mathrm{div}}}
\def \mod	{\z@bin{\mathrm{mod}}}
\def \succ	{\word{succ}}
\def \expon	{^}
%	aliases
\let \num	\integer
\let \nplus	\natone
%
%	LOGIC
%
\def \lnot	{\neg\;}
\def \land	{\z@rel{\wedge}}
\def \lor	{\z@rel{\vee}}
\let \imp	\Rightarrow
\let \iff	\Leftrightarrow
\def \all	{\z@op{\xforall}}
\def \exi	{\z@op{\xexists}}
\def \exione	{\exists_1}
\DeclareMathSymbol{\nexi}{\mathord}{AMSb}{"40}
\def \dot	{\z@rel{\bullet}}
\def \true	{\keyword{true}}
\def \false	{\keyword{false}}
\let \cond	\rightarrow
%	aliases
\let \spot	\dot
\mathcode`\@="8000% make @ active in mathmode
{\catcode`\@=\active \gdef@{\dot}}
\let \implies	\imp
\let \forall	\all
\let \exists	\exi
\let \nexists	\nexi
%
%	SETS
%
\let \emptyset  \varnothing
\def \varemptyset  {\{\,\}}
\def \pset	{\z@op{\bbold P}}
\def \psetone	{\pset_1}
\def \fset	{\z@op{\bbold F}}
\def \fsetone	{\fset_1}
\def \sset	{\z@op{\bbold S}}
\let \mem	\in
\def \nem	{\not\mem}
\def \uni	{\z@bin\cup}
\def \int	{\z@bin\cap}
\let \prod	\times
\def \min	{\word{min}}
\def \max	{\word{max}}
\def \duni	{\z@Bigop{\lower0.25ex\hbox{$\uni$}}}
\def \dint	{\z@Bigop{\lower0.25ex\hbox{$\int$}}}
\def \upto	{\z@bin{\ldotp\ldotp}}
\let \psubs	\subset
\let \subs	\subseteq
\let \psups	\supset
\let \sups	\supseteq
\def \diff	{\z@bin{\backslash}}
%	aliases
\let \cross	\prod
\let \notin	\nem
\let \nmem	\nem
\let \union	\uni
\let \inter	\int
\let \power	\pset
\let \finset	\fset
\let \dunion	\duni
\let \dinter	\dint
%
%	RELATIONS & FUNCTIONS
%
\def \lambda	{\z@op{\xlambda}}
\def \mu	{\z@op{\xmu}}
\def \dom	{\keyword{dom}}
\def \ran	{\keyword{ran}}
\def \id	{\keyword{id}}
\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	{^{-1}}
\def \limg	{(\!|}
\def \rimg	{|\!)}
\let \map	\mapsto
\let \rel	\leftrightarrow
\let \tfun	\rightarrow
\let \tinj	\rightarrowtail
\def \tsur	{\mathrel{\ooalign{$\tfun$\hfil\cr$\mkern4mu\tfun$}}}
\def \pfun	{\p\tfun}
\def \pinj	{\p\tinj}
\def \psur	{\p\tsur}
\def \ffun	{\f\tfun}
\def \finj	{\f\tinj}
\def \bij	{\mathrel{\ooalign{$\tinj$\hfil\cr$\mkern5mu\tfun$}}}
\def \tcl	{^+}
\def \rtcl	{^*}
\def \iter	{^}
%	aliases
\let \comp	\fcmp
\let \ndres	\dsub
\let \nrres	\rsub
\let \fun	\tfun
\let \inj	\tinj
\let \surj	\tsur
\let \psurj	\psur
%
%	SEQUENCES
%
\def \seq	{\keyword{seq}}
\def \seqone	{\seq_1}
\def \emptyseq  {\lseq\,\rseq}
\let \lseq	\langle
\let \rseq	\rangle
\def \head	{\word{head}}
\def \tail	{\word{tail}}
\def \front	{\word{front}}
\def \last	{\word{last}}
\def \rev	{\word{rev}}
\def \squash	{\word{squash}}
\def \next	{\keyword{next}}
\def \inseq	{\keyword{in}}
\DeclareMathSymbol{\@@cat}{\mathbin}{AMSa}{"61}
\def \cat	{\mathbin{\raise 0.8ex\hbox{$\mathchar\@@cat$}}}
\DeclareMathSymbol{\sres}{\mathbin}{AMSa}{"16}
\DeclareMathSymbol{\ires}{\mathbin}{AMSa}{"18}
\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 \disjoint	{\keyword{disjoint}}
\def \subseq	{\keyword{subseq}}
%	aliases
\let \filter	\sres
%
%	SCHEMAS
%
\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]}
%	aliases
\let \project	\zproject
\let \import	\sres
\let \semi	\zcmp
\let \hide	\zhide
%
%	BAGS
%
\let\buni\uplus
\def \emptybag  {\lbag\:\rbag}
\def \lbag	{[\![}
\def \rbag	{]\!]}
\def \bag	{\keyword{bag}}
\def \items	{\word{items}}
\let \inbag	\inseq
\def \bagcount	{\word{count}}
%
%	DEFINITIONS & DECLARATIONS
%
\def \ddef	{\z@rel{\;::=\;}}
\def \bbar	{\z@bigrel{|}}
\let \cbar	\mid
\def \lang	{\langle\!\langle}
\def \rang	{\rangle\!\rangle}
\def \sdef	{\z@rel{\widehat=}}
\def \defs	{\z@smallrel{==}}
\def \varsdef	{\z@rel\triangleq}
%	aliases
\let \sdefs	\sdef
\mathcode`\|=\mid
\let \ldata	\lang
\let \rdata	\rang
%
%	MISCELLANEOUS
%
\def \lblot     {\langle\!|}
\def \rblot     {|\!\rangle}
\def \IMP	{\boldword{Import}}
\let \env	\Rrightarrow
\def \zlet      {\boldword{let}}
\def \zin       {\boldword{in}}
\def \zwhere	{\boldword{where}}
%
%	QZED SUPPORT
%
\def\HOLE{\z@op{\hbox{$\lll\star\star\star\ggg$}}}
\def\landd{} % to support qzed editor
\def\semid{} % to support qzed editor
\def\qzed{\ifz@inclass\else\zed\fi}
\def\endqzed{\ifz@inclass\else\endzed\fi}
%
%	CLASSES
%
\def\qua{\mbox{::}}
\def\redef{\mbox{\bf ~redef}}
\def\Init{I\!\mbox{\footnotesize\em NIT}}
\def\Exit{E\!\mbox{\footnotesize\em XIT}}
\def\Internal{I\!\mbox{\em\footnotesize NTERNAL}}
\def\Aux{A\!\mbox{\footnotesize\em UX}}
\def\intern{\mbox{\sf i}}
%
%		------ OTHER SPECIAL NOTATION ------
%
%	PROOFS
%
\def\thrm{\z@rel\vdash}
\def\qed{\zsmall\Box}
\let\Qed\Box
\let\QED\square
\def\BLACKQED{\zsmall\blacksquare}
\let\ETH\qed
\def\TH{\boldword{Theorem}}
\def\LE{\boldword{Lemma}}
\def\PR{\boldword{Proof}}
\def\refines{\z@rel\sqsupseteq}
\def\defines{\z@rel\sqsubseteq}
\def\weakrefine{\z@rel{\raise0.2ex\rlap{\hbox{$\sqsupset$}}\lower1ex\hbox{$\sim$}}}
\def\weakdefine{\z@rel{\raise0.2ex\rlap{\hbox{$\sqsubset$}}\lower1ex\hbox{$\sim$}}}
%	aliases
\let\shows\thrm
%
%	OBJECT THEORY
%
\def\childof{\z@rel\xsucc}
\def\parentof{\z@rel\xprec}
\let\weaksubclass\succsim
\let\weaksupclass\precsim
\def\hasa{\z@rel{\mathord\xsucc\!\!\!\mathord\xsucc}}
\def\instancein{\z@rel{\mathord\xprec\!\!\!\mathord\xprec}}
\def\subtype{\z@rel\sqsubset}
\def\subtypeeq{\z@rel\sqsubseteq}
\def\suptype{\z@rel\sqsupset}
\def\suptypeeq{\z@rel\sqsupseteq}
%	aliases
\let\inherits\childof
\let\subclass\childof
\let\isa\childof
\let\supclass\parentof
\let\instantiates\hasa
\let\islikea\weaksubclass
%
%	TEMPORAL LOGIC
%
\def\atnext{\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\zSmall\bigcirc$}\kern0.01em\zSmall\bigcirc}
\def\atlast{\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\kern0.01em\mathord-$}\zSmall\bigcirc}
\def\always{\lower0.37ex\hbox{$\zbig\Box$}}
\def\uptilnow{\rlap{$\kern0.02em\mathord-$}\lower0.37ex\hbox{$\zbig\Box$}}
\def\eventually{\lower0.37ex\hbox{$\zbig\Diamond$}}
\def\previously{\rlap{$\kern0.04em\mathord-$}\lower0.37ex\hbox{$\zbig\Diamond$}}
%	aliases
\let\henceforth\always
%
%	ORDERS
%
\def \mono	{\keyword{monotonic}}
\def \porder	{\keyword{partial\_order}}
\def \torder	{\keyword{total\_order}}
%
\newbox\z@combox\newdimen\z@wdcalc
\def\comment{\@ifnextchar*{\z@leftcomment}{\z@comment}}
\def\z@comment#1{$\z@stopfield\z@addfield\z@startfield$%
\global\setbox\z@combox\hbox{\quad[{\sf #1}]}\z@wdcalc=\wd\z@combox%
\advance\z@wdcalc by \wd\z@curline\advance\z@wdcalc by \z@curindent%
\advance\z@wdcalc by \zedleftsep\advance\z@wdcalc by \zedlinethickness%
\advance\z@wdcalc by 2\zedindent\ifdim\z@wdcalc>\displaywidth\\%
\fi&\box\z@combox\ignorespaces}
\def\z@leftcomment*#1{\hbox{[{\sf #1}]}}
%
%---------------------------
%
%	SECTION 3	Z ENVIRONMENTS
%
%		------ MARGIN STACK ------
%
% define a stack of dimensions (50 elements)
%	can probably be made smaller when qzed filters its TeX output better
\newcount\z@stackmin
\newcount\z@stackmax
\newcount\z@stacktop
\newdimen\@gtempa \z@stackmin=\allocationnumber
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@getempa \z@stackmax=\allocationnumber
\dimen\z@stackmin=0pt

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

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

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

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

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

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

%
%		------ BOXED ENVIRONMENTS ------
%
%
%	SCHEMA			schema definitions
%
\def\schema#1{\z@inoutbox\z@topline{$\,#1\,$}}
\def\endschema{\z@botline \endzed \z@makeinner \z@nopar}
%
%	SCHEMA*			schema with no name
%
\@namedef{schema*}{\leftnamesfalse\z@inoutbox\z@topline{}}
\expandafter\let\csname endschema*\endcsname=\endschema
%
%	GENSCHEMA		generic schema definitions
%
\def\genschema#1#2{\z@inoutbox\z@topline{$\,#1\:[#2]\,$}}
\let\endgenschema=\endschema
%
%	AXDEF			'liberal' axiomatic definitions
%
\def\axdef{\z@inoutbox}
\def\endaxdef{\endzed\z@makeinner}
%
%	UNIQDEF			'unique' axiomatic definitions
%
\def\uniqdef{\leftnamesfalse\z@inoutbox\z@dbltopline{}}
\let\enduniqdef=\endschema
%
%	GENDEF			'generic' axiomatic definitions
%
\def\gendef#1{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,[#1]\,$}}
\let\endgendef=\endschema
%
%	CLASS
%
\def\class#1{\z@leavevmode\z@makeouter\z@inclasstrue
		\z@boxenv\z@topline{$\,#1\,$}}
\let\endclass\endschema
%
%	OP
%
\def\op{\z@inclasscheck\schema}
\let\endop\endschema
%
%	STATE
%
\def\state{\z@inclasscheck\vbox\bgroup\vskip-\ht\zstrutbox\vbox\bgroup\hbox\bgroup\@nameuse{schema*}}
\def\endstate{\endschema\egroup\egroup\egroup}
%
%	INIT
%
\def\init{\z@inclasscheck\schema{\Init}}
\let\endinit\endschema
%
%		------ OTHER ENVIRONMENTS ------
%
%	SIDEBYSIDE
%
% This should support an arbitary number of columns
%	\zedindent's proportion of \linewidth gives a practical limit
%
\def\sidebyside{\@ifnextchar[{\z@columns}{\z@columns[2]}}
\def\z@columns[#1]{\z@leavevmode\z@cols#1 \z@makeouter\z@narrow%
	$$\lineskip=0pt\z@incolstrue
	\predisplaysize\maxdimen
	\ifz@leftmargin\hskip-\zedindent\z@leftmarginfalse\fi
	\setbox0=\hbox to \linewidth\bgroup\z@zeroskips%
	\divide\zedbar by \z@cols \divide\zedleftsep by \z@cols
	\divide\zedtab by \z@cols \divide\linewidth by \z@cols
	\parbox[t]{\linewidth}\bgroup\z@wide}
%
\def\nextside{\egroup\hss\parbox[t]{\linewidth}\bgroup\z@wide}
%
\newdimen\z@temp
\def\endsidebyside{\egroup\egroup
	\z@temp\ht0 \advance\z@temp by \dp0\advance\z@temp by-\dp\zstrutbox
	\hbox{\raise\z@temp\box0}\endz@env\z@makeinner\z@nopar}
%
%	ZPAR
%
\def\zpar{\z@leavevmode
	\ifz@inenv\z@inclasstrue\fi% fudge to let zpar in all boxes
	\z@makeouter\z@changesize
	\advance\linewidth by -\z@curindent
	\advance\linewidth by -\wd\z@curline
	\hskip-\wd\z@curline\advance\linewidth by -\zedindent$$
	\ifz@leftmargin\hskip-\zedindent\fi% adjustment for first column
	\advance\displayindent by \zedindent
	\advance\displaywidth by -\zedindent
	\advance\displayindent by \z@curindent
	\advance\displayindent by \wd\z@curline
	\advance\displaywidth by -\z@curindent
	\advance\displaywidth by -\wd\z@curline
	\global\setbox\z@curline\hbox{}
	\z@narrow\parbox[b]{\linewidth}\bgroup\hfil\break}
\def\endzpar{\egroup$$\z@makeinner\z@nopar}
%
%	CLASSCOM
%
\def \classcom{\zpar\sf}
\let \endclasscom=\endzpar
%
%	PROOF
%
\def\proof{\zpar$\PR$\zpar}
\def\endproof{\endzpar\endzpar}
%
% Additional auxiliary macros
%
\def\zseq#1{\lseq #1 \rseq}
\def\zset#1{\{ #1 \}}
\def\zimg#1{\limg #1 \rimg}
\def\zsch#1{\lsch #1 \rsch}
\def\zimgset#1{\zimg\zset{#1}}
%</nfoz>
%<*nfloz>
% Oz with Lucida Maths
% 1. august 92
% 2. sep 92. edited after move of Greek in Lucida maths fonts
% 3. jan 93. for NFSS2
\typeout{<Style option \filename, \filedate> (Oz with Lucida Maths)}
%
%	This document is organised as follows:
%
%	SECTION 1	Z FONTS
%	SECTION 2	Z SYMBOLS
%	SECTION 3	Z ENVIRONMENTS
%
% Modification History:
%
%               The original zed.sty file was written by Mike Spivey.
%               These macros have been extensively modified to
%               include extra symbols and environments for Object-Z
%               and now have little resemblence to the original macros.
%               Mike Spivey has also extended his macros along
%               different lines for Z - the latest version of macros
%               are called fuzz.sty and come with a syntax checker for Z.
%               They can be purchased for a small fee from:
%                       mike@prg.oxford.ac.uk
%
%        87	original zed.sty file - Mike Spivey
%        88	modified to include extra symbols and environments - Paul King
%        88	modified to include macros for UQ editor - Ray Neucom
%    May 89	modified to include object-oriented constructs - PK
%    Jun 89	modified to automatically change Z symbol size - PK
% 27 Jul 89	removed spurious space from \@setsize - PK
%  3 Aug 89	adjust style of equation number field - PK
% 24 Aug 89     add optional field to topline and zedline for proofs - PK
% 15 Sep 89     added extra qed symbols, updated classcom and comment - PK
% 25 Sep 89	renamed z@[bB]ig to z[bB]ig and changed temporal symbols - PK
% 30 Sep 89	added \znewpage, \Infrule, removed space above state box - PK
% 12 Mar 90	changed \@setsize to work better for double-spaced text - PK
% 31 Mar 90	added definition for @ and \bool and redefined `;' - PK
%  9 May 90	changed \sdef to \varsdef, \sdef & \defs to Spivey's latest - PK
% 27 May 90	added \c{n}{text} - a tab like \t{n} with text at left - PK
% 29 May 90	added `corners' to boxes and \zedcornerheight - PK
% 11 Jul 90	added \rename*[y/x] and \zseq \zset ..., changed \zeq \zimp - PK
%  2 Aug 90     added subseq - PK
%  9 Nov 90	changed \M to hopefully interact better with spacing -  PK
% 24 Feb 92     changed to work with NFSS - SPQR
%               check out \@ifundefined at start to isolate differences
%---------------------------
% Please post any updates that you may make to this file to:
%	Paul King -- ACSnet: king@batserver.cs.uq.oz.au
%---------------------------
%
%	SECTION 1	Z FONTS
%
%
%
% 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
%
\newbox\strutbox@
\def\strut@{\copy\strutbox@}
\addto@hook\every@size{%
    \setbox\strutbox@\hbox{\lower.5\normallineskiplimit
         \vbox{\kern-\normallineskiplimit\copy\strutbox}}}
\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@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}}
%
%	WORD STYLES
% these need handling a bit differently in NFSS
%
\def\String#1{\hbox{`{\tt #1}'}}
\def\STRING#1{\hbox{``{\tt #1}''}}
\def\infix#1{\z@rel{{\underline{#1}}}}
\def\word#1{\z@op{#1}}
\def\keyword#1{\z@op{\mbox{\rm #1}}}
\def\boldword#1{\z@op{\mbox{\bf #1}}}
\def\underword#1{\z@op{{\underline{#1}}}}
\def\underkeyword#1{\z@op{{\underline{\mbox{\rm #1}}}}}
\def\underboldword#1{\z@op{{\underline{\mbox{\bf #1}}}}}

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

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

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

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

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

% \p and \f make arrows with 1 and 2 crossings resp.
\def\p#1{\mathrel{\ooalign{\hfil$\mapstochar\mkern 5mu$\hfil\cr$#1$}}}
\def\f#1{\mathrel{\ooalign{\hfil
	$\mapstochar\mkern 3mu\mapstochar\mkern 5mu$\hfil\cr$#1$}}}
%
%	------ AMSTEX SYMBOL DEFINITIONS ------
%
% do these before Z symbols so that we can use them in our special symbols
%
%
%
%		------ SPECIAL Z SYMBOLS ------
%
%	NUMBERS
%
\def \nat	{{\bbold N}}
\def \integer	{{\bbold Z}}
\def \natone	{{\bbold N}_1}
\def \real	{{\bbold R}}
\def \bool	{{\bbold B}}
\let \divides	\div
\def \div	{\z@bin{\mathrm{div}}}
\def \mod	{\z@bin{\mathrm{mod}}}
\def \succ	{\word{succ}}
\def \expon	{^}
%	aliases
\let \num	\integer
\let \nplus	\natone
%
%	LOGIC
%
\def \lnot	{\neg\;}
\def \land	{\z@rel{\wedge}}
\def \lor	{\z@rel{\vee}}
\let \imp	\Rightarrow
\DeclareMathSymbol{\iff}{3}{arrows}{"61}
\def \all	{\z@op{\xforall}}
\def \exi	{\z@op{\xexists}}
\def \exione	{\exists_1}
\DeclareMathSymbol{\nexi}{0}{arrows}{"20}
\def \dot	{\z@rel{\bullet}}
\def \true	{\keyword{true}}
\def \false	{\keyword{false}}
\let \cond	\rightarrow
%	aliases
\let \spot	\dot
\mathcode`\@="8000% make @ active in mathmode
{\catcode`\@=\active \gdef@{\dot}}
\let \implies	\imp
\let \forall	\all
\let \exists	\exi
\let \nexists	\nexi
%
%	SETS
%
\let \emptyset  \varnothing
\def \varemptyset  {\{\,\}}
\def \pset	{\z@op{\bbold P}}
\def \psetone	{\pset_1}
\def \fset	{\z@op{\bbold F}}
\def \fsetone	{\fset_1}
\def \sset	{\z@op{\bbold S}}
\let \mem	\in
\def \nem	{\not\mem}
\def \uni	{\z@bin\cup}
\def \int	{\z@bin\cap}
\let \prod	\times
\def \min	{\word{min}}
\def \max	{\word{max}}
\def \duni	{\z@Bigop{\lower0.25ex\hbox{$\uni$}}}
\def \dint	{\z@Bigop{\lower0.25ex\hbox{$\int$}}}
\def \upto	{\z@bin{\ldotp\ldotp}}
\let \psubs	\subset
\let \subs	\subseteq
\let \psups	\supset
\let \sups	\supseteq
\def \diff	{\z@bin{\backslash}}
%	aliases
\let \cross	\prod
\let \notin	\nem
\let \nmem	\nem
\let \union	\uni
\let \inter	\int
\let \power	\pset
\let \finset	\fset
\let \dunion	\duni
\let \dinter	\dint
%
%	RELATIONS & FUNCTIONS
%
\def \lambda	{\z@op{\xlambda}}
\def \mu	{\z@op{\xmu}}
\def \dom	{\keyword{dom}}
\def \ran	{\keyword{ran}}
\def \id	{\keyword{id}}
\@mc \dres	"212F
\@mc \rres	"212E
\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	{^{-1}}
\def \limg	{(\!|}
\def \rimg	{|\!)}
\let \map	\mapsto
\let \rel	\leftrightarrow
\let \tfun	\rightarrow
\let \tinj	\rightarrowtail
\def \tsur	{\mathrel{\ooalign{$\tfun$\hfil\cr$\mkern4mu\tfun$}}}
\def \pfun	{\p\tfun}
\def \pinj	{\p\tinj}
\def \psur	{\p\tsur}
\def \ffun	{\f\tfun}
\def \finj	{\f\tinj}
\def \bij	{\mathrel{\ooalign{$\tinj$\hfil\cr$\mkern5mu\tfun$}}}
\def \tcl	{^+}
\def \rtcl	{^*}
\def \iter	{^}
%	aliases
\let \comp	\fcmp
\let \ndres	\dsub
\let \nrres	\rsub
\let \fun	\tfun
\let \inj	\tinj
\let \surj	\tsur
\let \psurj	\psur
%

\@mc \lll	"31DE
\let \llless	\lll
\@mc \ggg	"31DF
\let \gggtr	\ggg
%
% already in lucidab
%\def\checkmark{\mathhexbox\thearfam AC }
%\def \circledR	{\mathhexbox1C9 }
%\def \maltese	{\mathhexbox1CB }
\@mc \eth	"00F0   % in Cork layout only!
\def \interleave	{{\parallel\!\!\vert}}
\def \shortinterleave	{\z@rel{\mathord\shortmid\mathord\shortparallel}}
\let \restriction	\upharpoonright
\@mc \doublebarwedge	"22D4
\def \napprox	{\not\approx}

%	SEQUENCES
%
\def \seq	{\keyword{seq}}
\def \seqone	{\seq_1}
\def \emptyseq  {\lseq\,\rseq}
\let \lseq	\langle
\let \rseq	\rangle
\def \head	{\word{head}}
\def \tail	{\word{tail}}
\def \front	{\word{front}}
\def \last	{\word{last}}
\def \rev	{\word{rev}}
\def \squash	{\word{squash}}
\def \next	{\keyword{next}}
\def \inseq	{\keyword{in}}
\def \cat	{\mathbin{\raise 0.8ex\hbox{$\mathchar"215F$}}}
\DeclareMathSymbol{\sres}{2}{arrows}{"75}
\def \ssub	{\z@bin{\rlap{$-$}{\sres}}}
\DeclareMathSymbol{\ires}{2}{arrows}{"76}
\def \isub	{\z@bin{\rlap{$-$}{\ires}}}
\def \dcat	{\z@op{\cat/}}
\def \dovr	{\z@op{\fovr/}}
\def \dcmp	{\z@op{\fcmp/}}
\let \prefix	\subseteq
\def \suffix	{\keyword{suffix}}
\def \seqi	{\keyword{seq_\infty}}
\def \partitions	{\keyword{partitions}}
\def \disjoint	{\keyword{disjoint}}
\def \subseq	{\keyword{subseq}}
%	aliases
\let \filter	\sres
%
%	SCHEMAS
%
\def \lsch	{\z@bigop{[}}
\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]}
%	aliases
\let \project	\zproject
\let \import	\sres
\let \semi	\zcmp
\let \hide	\zhide
%
%	BAGS
%
\let\buni\uplus
\def \emptybag  {\lbag\:\rbag}
\def \lbag	{[\![}
\def \rbag	{]\!]}
\def \bag	{\keyword{bag}}
\def \items	{\word{items}}
\let \inbag	\inseq
\def \bagcount	{\word{count}}
%
%	DEFINITIONS & DECLARATIONS
%
\def \ddef	{\z@rel{\;::=\;}}
\def \bbar	{\z@bigrel{|}}
\let \cbar	\mid
\def \lang	{\langle\!\langle}
\def \rang	{\rangle\!\rangle}
\def \sdef	{\z@rel{\widehat=}}
\def \defs	{\z@smallrel{==}}
\def \varsdef	{\z@rel\triangleq}
%	aliases
\let \sdefs	\sdef
\mathcode`\|=\mid
\let \ldata	\lang
\let \rdata	\rang
%
%	MISCELLANEOUS
%
\def \lblot     {\langle\!|}
\def \rblot     {|\!\rangle}
\def \IMP	{\boldword{Import}}
\let \env	\Rrightarrow
\def \zlet      {\boldword{let}}
\def \zin       {\boldword{in}}
\def \zwhere	{\boldword{where}}
%
%	QZED SUPPORT
%
\def\HOLE{\z@op{\hbox{$\lll\star\star\star\ggg$}}}
\def\landd{} % to support qzed editor
\def\semid{} % to support qzed editor
\def\qzed{\ifz@inclass\else\zed\fi}
\def\endqzed{\ifz@inclass\else\endzed\fi}
%
%	CLASSES
%
\def\qua{\mbox{::}}
\def\redef{\mbox{\bf ~redef}}
\def\Init{I\!\mbox{\footnotesize\em NIT}}
\def\Exit{E\!\mbox{\footnotesize\em XIT}}
\def\Internal{I\!\mbox{\em\footnotesize NTERNAL}}
\def\Aux{A\!\mbox{\footnotesize\em UX}}
\def\intern{\mbox{\sf i}}
%
%		------ OTHER SPECIAL NOTATION ------
%
%	PROOFS
%
\def\thrm{\z@rel\vdash}
\def\qed{\zsmall\Box}
\let\Qed\Box
\let\QED\square
\def\BLACKQED{\zsmall\blacksquare}
\let\ETH\qed
\def\TH{\boldword{Theorem}}
\def\LE{\boldword{Lemma}}
\def\PR{\boldword{Proof}}
\def\refines{\z@rel\sqsupseteq}
\def\defines{\z@rel\sqsubseteq}
\def\weakrefine{\z@rel{\raise0.2ex\rlap{\hbox{$\sqsupset$}}\lower1ex\hbox{$\sim$}}}
\def\weakdefine{\z@rel{\raise0.2ex\rlap{\hbox{$\sqsubset$}}\lower1ex\hbox{$\sim$}}}
%	aliases
\let\shows\thrm
%
%	OBJECT THEORY
%
\def\childof{\z@rel\xsucc}
\def\parentof{\z@rel\xprec}
\let\weaksubclass\succsim
\let\weaksupclass\precsim
\def\hasa{\z@rel{\mathord\xsucc\!\!\!\mathord\xsucc}}
\def\instancein{\z@rel{\mathord\xprec\!\!\!\mathord\xprec}}
\def\subtype{\z@rel\sqsubset}
\def\subtypeeq{\z@rel\sqsubseteq}
\def\suptype{\z@rel\sqsupset}
\def\suptypeeq{\z@rel\sqsupseteq}
%	aliases
\let\inherits\childof
\let\subclass\childof
\let\isa\childof
\let\supclass\parentof
\let\instantiates\hasa
\let\islikea\weaksubclass
%
%	TEMPORAL LOGIC
%
\def\atnext{\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\zSmall\bigcirc$}\kern0.01em\zSmall\bigcirc}
\def\atlast{\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\kern0.01em\mathord-$}\zSmall\bigcirc}
\def\always{\lower0.37ex\hbox{$\zbig\Box$}}
\def\uptilnow{\rlap{$\kern0.02em\mathord-$}\lower0.37ex\hbox{$\zbig\Box$}}
\def\eventually{\lower0.37ex\hbox{$\zbig\Diamond$}}
\def\previously{\rlap{$\kern0.04em\mathord-$}\lower0.37ex\hbox{$\zbig\Diamond$}}
%	aliases
\let\henceforth\always
%
%	ORDERS
%
\def \mono	{\keyword{monotonic}}
\def \porder	{\keyword{partial\_order}}
\def \torder	{\keyword{total\_order}}
%
\newbox\z@combox\newdimen\z@wdcalc
\def\comment{\@ifnextchar*{\z@leftcomment}{\z@comment}}
\def\z@comment#1{$\z@stopfield\z@addfield\z@startfield$%
\global\setbox\z@combox\hbox{\quad[{\sf #1}]}\z@wdcalc=\wd\z@combox%
\advance\z@wdcalc by \wd\z@curline\advance\z@wdcalc by \z@curindent%
\advance\z@wdcalc by \zedleftsep\advance\z@wdcalc by \zedlinethickness%
\advance\z@wdcalc by 2\zedindent\ifdim\z@wdcalc>\displaywidth\\%
\fi&\box\z@combox\ignorespaces}
\def\z@leftcomment*#1{\hbox{[{\sf #1}]}}
%
%---------------------------
%
%	SECTION 3	Z ENVIRONMENTS
%
%		------ MARGIN STACK ------
%
% define a stack of dimensions (50 elements)
%	can probably be made smaller when qzed filters its TeX output better
\newcount\z@stackmin
\newcount\z@stackmax
\newcount\z@stacktop
\newdimen\@gtempa \z@stackmin=\allocationnumber
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@getempa \z@stackmax=\allocationnumber
\dimen\z@stackmin=0pt

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

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

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

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

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

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

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

%<*nflucbrb>
% this is for Berry-type font names
\immediate\write\sixt@@n{File: `nflucbrb.sty'}
\renewcommand{\sfdefault}{hlcs}
\renewcommand{\rmdefault}{hlc}
\renewcommand{\ttdefault}{hlct}
\def\bfdefault{b}
\def\encodingdefault{T1}% 
\fontencoding{T1}% 
% NOTE: all depends on the character encoding used in the plain text
% fonts! Whatever you set as \defaultencoding will determine the effect.
% If you use Y&Y's example tfm files, you may wish to change
% \Encoding here to be, eg, OT1, and \input stanacce.
% If you prefer `texannew' encoding in accents.tex, better
% define a new encoding scheme for NFSS2 and switch to that.
%
% new encoding scheme for Math Arrows font
\DeclareFontEncoding{MR}{}{}
\DeclareFontSubstitution{MR}{hlcm}{m}{n}
\DeclareSymbolFont{letters}{OML}{hlcm}{m}{it}
\DeclareSymbolFont{symbols}{OMS}{hlcm}{m}{n}
\DeclareSymbolFont{largesymbols}{OMX}{hlcm}{m}{n}
\SetSymbolFont{letters}{bold}{OML}{hlcm}{m}{it}%
%
% better get the order of this right, or maths come out as all arrows..
%
\DeclareSymbolFont{italics}{\encodingdefault}{\rmdefault}{m}{it}
\DeclareSymbolFont{arrows}{MR}{hlcm}{m}{n}
%</nflucbrb>
%<*nflucbry>
% this is for Y&Y font names
\immediate\write\sixt@@n{File: `nflucbry.sty'}
\renewcommand{\sfdefault}{lbs}
\renewcommand{\rmdefault}{lb}
\renewcommand{\ttdefault}{lbt}
\def\bfdefault{b}
\def\encodingdefault{OT1}% 
\fontencoding{OT1}% 
% NOTE: all depends on the character encoding used in the plain text
% fonts! Whatever you set as \defaultencoding will determine the effect.
% new encoding scheme for Math Arrows font
%
\DeclareFontEncoding{MR}{}{}
\DeclareFontSubstitution{MR}{hlcm}{m}{n}
\DeclareSymbolFont{letters}{OML}{lbm}{m}{it}
\DeclareSymbolFont{symbols}{OMS}{lbm}{m}{n}
\DeclareSymbolFont{largesymbols}{OMX}{lbm}{m}{n}
\SetSymbolFont{letters}{bold}{OML}{lbm}{m}{it}
%
% better get the order of this right, or maths come out as all arrows..
%
\DeclareSymbolFont{italics}{\encodingdefault}{\rmdefault}{m}{it}
\DeclareSymbolFont{arrows}{MR}{lbm}{m}{n}
%</nflucbry>
%<*lucidabright>
%--------------------------------------------------------------------
%
%
% allow for scaling of Lucida Bright. Tug93 used .94 to match space
% taken by CMR
\def\LucidaScale{1}
% Adjusted for LucidaNewMath-Extension at 9.5pt and math axis at 313
% Note: delimiter increments are 5.5pt (as opposed to 6pt in CM)
\def\Lucidasizes{%
  \def\@vpt{5.2}%
  \def\@vipt{6.1}%
  \def\@viipt{6.9}%
  \def\@viiipt{7.8}%
  \def\@ixpt{8.6}%
  \def\@xpt{9.5}%
  \def\@xipt{10.4}%
  \def\@xiipt{11.2}%
  \def\@xivpt{12.9}%
  \def\@xviipt{15.5}%
  \def\@xxpt{18.1}%
  \def\@xxvpt{22.4}%
 \define@mathsizes{5.2}{5.2}{5.2}
 \define@mathsizes{6.1}{5.2}{5.2}
 \define@mathsizes{6.9}{5.2}{5.2}
 \define@mathsizes{7.8}{6.1}{5.2}
 \define@mathsizes{8.6}{6.1}{5.2}
 \define@mathsizes{9.5}{6.9}{5.2}
 \define@mathsizes{10.95}{6.9}{5.2}
 \define@mathsizes{11.2}{7.8}{6.1}
 \define@mathsizes{12.9}{9.5}{6.9}
 \define@mathsizes{15.5}{11.2}{9.5}
 \define@mathsizes{18.1}{12.9}{11.2}
 \define@mathsizes{22.4}{18.1}{15.5}
}%
\def\CMRsizes{%
 \def\@vpt{5}%
 \def\@vipt{6}%
 \def\@viipt{7}%
 \def\@viiipt{8}%
 \def\@ixpt{9}%
 \def\@xpt{10}%
 \def\@xipt{11}%
 \def\@xiipt{12}%
 \def\@xivpt{14}%
 \def\@xviipt{17}%
 \def\@xxpt{20}%
 \def\@xxvpt{25}%
}%

\Lucidasizes
%
\DeclareSymbolFont{operators}{\encodingdefault}{\rmdefault}{m}{n}
%
\SetSymbolFont{operators}{bold}{\encodingdefault}{\rmdefault}{b}{n}%
\SetSymbolFont{operators}{normal}{\encodingdefault}{\rmdefault}{m}{n}%
\SetMathAlphabet{\mathbf}{normal}{\encodingdefault}{\rmdefault}{b}{n}%
\SetMathAlphabet{\mathsf}{normal}{\encodingdefault}{\sfdefault}{m}{n}%
\SetMathAlphabet{\mathrm}{normal}{\encodingdefault}{\rmdefault}{m}{n}%
\SetMathAlphabet{\mathbf}{bold}{\encodingdefault}{\rmdefault}{m}{n}%
\SetMathAlphabet{\mathsf}{bold}{\encodingdefault}{\sfdefault}{b}{n}%
\SetMathAlphabet{\mathrm}{bold}{\encodingdefault}{\rmdefault}{b}{n}%
\DeclareSymbolFontAlphabet{\lbit}{italics}
%
\DeclareSymbolFontAlphabet{\bbold}{arrows}
%
% *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** 
% 	This section derives mostly from lcdmacro.tex and amssymblb.tex
%	Copyright (C) 1991, 1992 Y&Y. All Rights Reserved
% 		Version 1.2 		1992 June 14
% *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** 
% Some modifications due to Bram de Jager
% *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** %
\expandafter\ifx\csname amsfonts.sty\endcsname\relax %MJD%
% %MJD% Then amsfonts.sty is not in use.
  \def\big#1{{\hbox{$\left#1\vbox to8.20\p@{}\right.\n@space$}}}
  \def\Big#1{{\hbox{$\left#1\vbox to10.80\p@{}\right.\n@space$}}}
  \def\bigg#1{{\hbox{$\left#1\vbox to13.42\p@{}\right.\n@space$}}}
  \def\Bigg#1{{\hbox{$\left#1\vbox to16.03\p@{}\right.\n@space$}}}
  \def\biggg#1{{\hbox{$\left#1\vbox to17.72\p@{}\right.\n@space$}}}
  \def\Biggg#1{{\hbox{$\left#1\vbox to21.25\p@{}\right.\n@space$}}}
  \def\n@space{\nulldelimiterspace\z@ \m@th}
\else %MJD%
% %MJD% It's possible the factors 1.5, 2, 2.5, 3, 3.5 should be adjusted
% %MJD% for Lucida fonts. But that has to be determined by looking at
% %MJD% printed tests which I cannot do at the moment. [mjd,24-Jun-1993]
  \def\biggg{\bBigg@\thr@@} %MJD%
  \def\Biggg{\bBigg@{3.5}} %MJD%
\fi %MJD%

% define some extra large sizes - always done using extensible parts

\def\bigggl{\mathopen\biggg}
\def\bigggr{\mathclose\biggg}
\def\Bigggl{\mathopen\Biggg}
\def\Bigggr{\mathclose\Biggg}
%
%  Following is only really needed if the roman text font is NOT LucidaBright
%  Draw the small sizes of `[' and `]' from math italic instead of roman font

\mathcode`\[="4186 \delcode`\[="186302 
\mathcode`\]="5187 \delcode`\]="187303

%  Draw the small sizes of `(' and `)' from math italic instead of roman font
\mathcode`\(="4184 \delcode`\(="184300
\mathcode`\)="5185 \delcode`\)="185301

%  Draw  `=' and `+' from symbol font instead of roman
\mathcode`\=="3283 
\mathcode`\+="2282

% Draw small `/' from math italic instead of roman font
\mathcode`\/="013D \delcode`\/="13D30E

% *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** %
% Make open face brackets accessible, i.e. [[ and ]]

\def\ldbrack{\delimiter"4182382}
\def\rdbrack{\delimiter"5183383}

% Provide access to surface integral signs (linked from text to display size)
\mathchardef\surfintop="1390 
\def\surfint{\surfintop\nolimits}

% Make medium size integrals available (NOT linked to display size)
\mathchardef\midintop="1392 \def\midint{\midintop\nolimits}
\mathchardef\midointop="1393 \def\midoint{\midointop\nolimits}
\mathchardef\midsurfintop="1394 \def\midsurfint{\midsurfintop\nolimits}

% Extensible integral (use with \bigg, \Bigg, \biggg, \Biggg etc)

\def\largeint{\delimiter"135A395}

% Various types of small integrals

% \mathchardef\dblint="0188
% \mathchardef\trplint="0189
% \mathchardef\contint="018A
% \mathchardef\surfint="018B
% \mathchardef\volint="018C
% \mathchardef\clwint="018D
% \mathchardef\cclwcint="018E
% \mathchardef\clwcint="018F

% *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** %

% To close up gaps in special math characters constructed from pieces
\def\joinrel{\mathrel{\mkern-4mu}} % \def\joinrel{\mathrel{\mkern-3mu}}

% Some characters that need construction in CM exist complete in math
% italic or math symbol font
\mathchardef\bowtie="31F6
\mathchardef\models="32EE
\mathchardef\doteq="32C9
\mathchardef\cong="329B
\mathchardef\angle="028B
% these need undefining so that we can redeclare them
\let\Box\undefined
\let\Diamond\undefined
\let\leadsto\undefined
\let\neq\undefined
\let\hookleftarrow\undefined
\let\hookrightarrow\undefined
\let\mapsto\undefined
\let\notin\undefined
\let\circle\undefined
\let\iff\undefined
\let\rightleftharpoons\undefined
% Other characters may be found in LucidaNewMath-Arrows (more negated later)
\DeclareMathSymbol{\neq}{3}{arrows}{"94}
\DeclareMathSymbol{\rightleftharpoons}{3}{arrows}{"7A}
\DeclareMathSymbol{\leftrightharpoons}{3}{arrows}{"79}
\DeclareMathSymbol{\hookleftarrow}{3}{arrows}{"3C}
\DeclareMathSymbol{\hookrightarrow}{3}{arrows}{"3E}
\DeclareMathSymbol{\mapsto}{3}{arrows}{"2C}
\def\longmapsto{\mapstochar\longrightarrow}

% *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** %

% SPECIAL LaTeX character definitions (originally from LaTeX symbol font)

\mathchardef\mho"0192
\mathchardef\Join"31F6
\mathchardef\sqsubset"32E4
\mathchardef\sqsupset"32E5

\mathchardef\rhd"312E
\mathchardef\lhd"312F
\mathchardef\unlhd"32F4
\mathchardef\unrhd"32F5

\DeclareMathSymbol{\Box}{0}{arrows}{"02} 
\DeclareMathSymbol{\Diamond}{0}{arrows}{"08}
\DeclareMathSymbol{\leadsto}{3}{arrows}{"8E} 
\DeclareMathSymbol{\leadsfrom}{3}{arrows}{"8D}

\def\mathstrut{\vphantom{f}}
\expandafter\ifx\csname amstex.sty\endcsname\relax %MJD%
% %MJD% Then amstex.sty not in use: modify \matrix it to adjust the
% %MJD% first and last line vertical spacing slightly; otherwise leave
% %MJD% it alone.
%
% following changed because fonts (i.e. math italic) not `at full scale'
  \def\matrix#1{\null\,\vcenter{\normalbaselines\m@th
    \ialign{\hfil$##$\hfil&&\quad\hfil$##$\hfil\crcr
      \mathstrut\crcr\noalign{\kern-0.9\baselineskip}
     #1\crcr\mathstrut\crcr\noalign{\kern-0.9\baselineskip}}}\,}
\fi %MJD%

% In n-th root, don't want the `n' to come too close to the radical

\def\r@@t#1#2{\setbox\z@\hbox{$\m@th#1\sqrt{#2}$}
  \dimen@\ht\z@ \advance\dimen@-\dp\z@
  \mkern5mu\raise.6\dimen@\copy\rootbox \mkern-7.5mu \box\z@}

% The following are the standard plain TeX defaults for CM

% \delimiterfactor=901
% \delimitershortfall=5pt
% \nulldelimiterspace=1.2pt
% \scriptspace=0.5pt
% \thinmuskip=3mu
% \medmuskip=4mu plus 2mu minus 4mu
% \thickmuskip=5mu plus 5mu

% Here are some extra definitions of mathematical symbols and operators

% {\buildrel \rm def \over =}
\mathchardef\defineequal"32D6

% Here are some negated operators from LucidaNewMath-Arrows:

\DeclareMathSymbol{\notleq}{3}{arrows}{"9C}
\DeclareMathSymbol{\notgeq}{3}{arrows}{"9D}
\DeclareMathSymbol{\notequiv}{3}{arrows}{"95}
\DeclareMathSymbol{\notprec}{3}{arrows}{"E5}
\DeclareMathSymbol{\notsucc}{3}{arrows}{"E6}
\DeclareMathSymbol{\notapprox}{3}{arrows}{"98}
\DeclareMathSymbol{\notpreceq}{3}{arrows}{"E7}
\DeclareMathSymbol{\notsucceq}{3}{arrows}{"E8}
\DeclareMathSymbol{\notasymp}{3}{arrows}{"F3}
\DeclareMathSymbol{\notsubset}{3}{arrows}{"C6}
\DeclareMathSymbol{\notsupset}{3}{arrows}{"C7}
\DeclareMathSymbol{\notsim}{3}{arrows}{"96}
\DeclareMathSymbol{\notsubseteq}{3}{arrows}{"C8}
\DeclareMathSymbol{\notsupseteq}{3}{arrows}{"C9}
\DeclareMathSymbol{\notsimeq}{3}{arrows}{"97}
\DeclareMathSymbol{\notsqsubseteq}{3}{arrows}{"D4}
\DeclareMathSymbol{\notsqsupseteq}{3}{arrows}{"D5}
\DeclareMathSymbol{\notcong}{3}{arrows}{"99}
\DeclareMathSymbol{\notin}{3}{arrows}{"1D}
\DeclareMathSymbol{\notni}{3}{arrows}{"1F}
\DeclareMathSymbol{\notvdash}{3}{arrows}{"F8}
\DeclareMathSymbol{\notmodels}{3}{arrows}{"F9}
\DeclareMathSymbol{\notparallel}{3}{arrows}{"F7}
\DeclareMathSymbol{\noteq}{3}{arrows}{"94}
\DeclareMathSymbol{\notless}{3}{arrows}{"9A}
\DeclareMathSymbol{\notgreater}{3}{arrows}{"9B}
\DeclareMathSymbol{\notmid}{3}{arrows}{"F6}

% *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** %

% Now for some AMS TeX items

% Start with black-board bold (open face) characters

\expandafter\ifx\csname amsfonts.sty\endcsname\relax %MJD%
% %MJD% Then amsfonts.sty not in use.
  \def\nonmatherr@#1{\errmessage{\string#1\space allowed only in math mode}}
  \def\Bbb{\relax\ifmmode\expandafter\Bbb@\else
   \expandafter\nonmatherr@\expandafter\Bbb\fi}
\fi %MJD%
\let\Bbb@\bbold

% \DeclareMathSymbol{\Bbbk}{0}{arrows}{"6B}

% lplain.tex draws upper case (upright) greek from cmr10 ---
% when using the Cork encoding, that isn't there, so its been put
% in the extension font (largesymbols)
\DeclareMathSymbol{\Gamma}{0}{largesymbols}{'320}
\DeclareMathSymbol{\Delta}{0}{largesymbols}{'321}
\DeclareMathSymbol{\Theta}{0}{largesymbols}{'322}
\DeclareMathSymbol{\Lambda}{0}{largesymbols}{'323}
\DeclareMathSymbol{\Xi}{0}{largesymbols}{'324}
\DeclareMathSymbol{\Pi}{0}{largesymbols}{'325}
\DeclareMathSymbol{\Sigma}{0}{largesymbols}{'326}
\DeclareMathSymbol{\Upsilon}{0}{largesymbols}{'327}
\DeclareMathSymbol{\Phi}{0}{largesymbols}{'330}
\DeclareMathSymbol{\Psi}{0}{largesymbols}{'331}
\DeclareMathSymbol{\Omega}{0}{largesymbols}{'332}

\mathchardef\varGamma="0100
\mathchardef\varDelta="0101
\mathchardef\varTheta="0102
\mathchardef\varLambda="0103
\mathchardef\varXi="0104
\mathchardef\varPi="0105
\mathchardef\varSigma="0106
\mathchardef\varUpsilon="0107
\mathchardef\varPhi="0108
\mathchardef\varPsi="0109
\mathchardef\varOmega="010A
%
% Definitions for math symbols and operators 
%  --- normally found in the fonts MSAM* and MSBM* ---
%  using LucidaNewMath fonts 
%  Definitions followed by question marks represent less than ideal matches.
% MSAM* equivalents

\mathchardef\boxdot="22ED
\mathchardef\boxplus="22EA
\mathchardef\boxtimes="22EC
\DeclareMathSymbol{\square}{0}{arrows}{"02}
\DeclareMathSymbol{\blacksquare}{0}{arrows}{"03}
%\DeclareMathSymbol{\circle}{0}{arrows}{"00}
%\DeclareMathSymbol{\blackcircle}{0}{arrows}{"01}
\DeclareMathSymbol{\centerdot}{2}{arrows}{"E1}
\DeclareMathSymbol{\lozenge}{0}{arrows}{"08}
\DeclareMathSymbol{\blacklozenge}{0}{arrows}{"09}
\DeclareMathSymbol{\circlearrowright}{3}{arrows}{"8C}
\DeclareMathSymbol{\circlearrowleft}{3}{arrows}{"8B}
\DeclareMathSymbol{\rightleftharpoons}{3}{arrows}{"7A}
\DeclareMathSymbol{\leftrightharpoons}{3}{arrows}{"79}
\mathchardef\boxminus="22EB
\mathchardef\Vdash="32F0
\mathchardef\Vvdash="31D3
\mathchardef\vDash="32EE
\DeclareMathSymbol{\twoheadrightarrow}{3}{arrows}{"25}
\DeclareMathSymbol{\twoheadleftarrow}{3}{arrows}{"23}
\DeclareMathSymbol{\leftleftarrows}{3}{arrows}{"71}
\DeclareMathSymbol{\rightrightarrows}{3}{arrows}{"73}
\DeclareMathSymbol{\upuparrows}{3}{arrows}{"72}
\DeclareMathSymbol{\downdownarrows}{3}{arrows}{"74}
\DeclareMathSymbol{\upharpoonright}{3}{arrows}{"75}
\DeclareMathSymbol{\downharpoonright}{3}{arrows}{"77}
\DeclareMathSymbol{\upharpoonleft}{3}{arrows}{"76}
\DeclareMathSymbol{\downharpoonleft}{3}{arrows}{"78}
\DeclareMathSymbol{\rightarrowtail}{3}{arrows}{"29}
\DeclareMathSymbol{\leftarrowtail}{3}{arrows}{"28}
\DeclareMathSymbol{\leftrightarrows}{3}{arrows}{"6E}
\DeclareMathSymbol{\rightleftarrows}{3}{arrows}{"6D}
\DeclareMathSymbol{\Lsh}{3}{arrows}{"7B}
\DeclareMathSymbol{\Rsh}{3}{arrows}{"7D}
\DeclareMathSymbol{\rightsquigarrow}{3}{arrows}{"8E}
\DeclareMathSymbol{\leftsquigarrow}{3}{arrows}{"8D}
\DeclareMathSymbol{\leftrightsquigarrow}{3}{arrows}{"91}
\DeclareMathSymbol{\looparrowleft}{3}{arrows}{"3F}
\DeclareMathSymbol{\looparrowright}{3}{arrows}{"40}
\mathchardef\circeq="32D0
\mathchardef\succsim="32E1
\mathchardef\gtrsim="32DD
\mathchardef\gtrapprox="31DB
\mathchardef\multimap="31C7
\mathchardef\image="31C6
\mathchardef\original="31C5
\mathchardef\therefore="3290
\mathchardef\because="3291
\mathchardef\doteqdot="32CA
\mathchardef\triangleq="32D5
\mathchardef\precsim="32E0
\mathchardef\lesssim="32DC
\mathchardef\lessapprox="31DA
\mathchardef\eqslantless="31E2
\mathchardef\eqslantgtr="31E3
\mathchardef\curlyeqprec="31E6
\mathchardef\curlyeqsucc="31E7
\mathchardef\preccurlyeq="31E4
\mathchardef\leqq="32DA
\mathchardef\leqslant="31E0
\mathchardef\lessgtr="32DE
\mathchardef\backprime="01C8
\DeclareMathSymbol{\axisshort}{0}{arrows}{"39}
\mathchardef\risingdotseq="32CC
\mathchardef\fallingdotseq="32CB
\mathchardef\succcurlyeq="31E5
\mathchardef\geqq="32DB
\mathchardef\geqslant="31E1
\mathchardef\gtrless="32DF
\mathchardef\sqsubset="32E4
\mathchardef\sqsupset="32E5
\mathchardef\vartriangleright="312E
\mathchardef\vartriangleleft="312F
\mathchardef\trianglerighteq="32F5
\mathchardef\trianglelefteq="32F4
\DeclareMathSymbol{\bigstar}{0}{arrows}{"AB}
\mathchardef\between="31F2
\DeclareMathSymbol{\blacktriangledown}{0}{arrows}{"07}
\mathchardef\blacktriangleright="31F1
\mathchardef\blacktriangleleft="31F0
\DeclareMathSymbol{\arrowaxisright}{0}{arrows}{"37}
\DeclareMathSymbol{\arrowaxisleft}{0}{arrows}{"36}
\DeclareMathSymbol{\vartriangle}{3}{arrows}{"04}
\DeclareMathSymbol{\blacktriangle}{0}{arrows}{"05}
\DeclareMathSymbol{\triangledown}{0}{arrows}{"06}
\mathchardef\eqcirc="32CF
\mathchardef\lesseqgtr="31E8
\mathchardef\gtreqless="31E9
\mathchardef\lesseqqgtr="31EA
\mathchardef\gtreqqless="31EB
\DeclareMathSymbol{\Rrightarrow}{3}{arrows}{"6C}
\DeclareMathSymbol{\Lleftarrow}{3}{arrows}{"6A}
\mathchardef\veebar="21D2
\mathchardef\barwedge="22F6
\mathchardef\angle="028B
\mathchardef\measuredangle="028C
\mathchardef\sphericalangle="028D
\mathchardef\varpropto="322F % ?
\mathchardef\smallsmile="315E % ? 
\mathchardef\smallfrown="315F % ?	
\mathchardef\Subset="32F8
\mathchardef\Supset="32F9
\mathchardef\Cup="22FA
\mathchardef\Cap="22FB
\mathchardef\curlywedge="2284
\mathchardef\curlyvee="2285
\mathchardef\leftthreetimes="21D0
\mathchardef\rightthreetimes="21D1
\mathchardef\subseteqq="31EE
\mathchardef\supseteqq="31EF
\mathchardef\bumpeq="32C8
\mathchardef\Bumpeq="32C7
\mathchardef\lll="31DE
\mathchardef\ggg="31DF
\mathchardef\circledS="01CA
\mathchardef\pitchfork="31F3
\mathchardef\dotplus="2289
\mathchardef\backsim="31F8
\mathchardef\backsimeq="31F9
\mathchardef\complement="0194
\mathchardef\intercal="21D9
\mathchardef\circledcirc="22E6
\mathchardef\circledast="22E7
\mathchardef\circleddash="21CC

% MSBM* equivalents

\DeclareMathSymbol{\lvertneqq}{3}{arrows}{"DE}
\DeclareMathSymbol{\gvertneqq}{3}{arrows}{"DF}
\DeclareMathSymbol{\nleq}{3}{arrows}{"9C}
\DeclareMathSymbol{\ngeq}{3}{arrows}{"9D}
\DeclareMathSymbol{\nless}{3}{arrows}{"9A}
\DeclareMathSymbol{\ngtr}{3}{arrows}{"9B}
\DeclareMathSymbol{\nprec}{3}{arrows}{"E5}
\DeclareMathSymbol{\nsucc}{3}{arrows}{"E6}
\DeclareMathSymbol{\lneqq}{3}{arrows}{"DC}
\DeclareMathSymbol{\gneqq}{3}{arrows}{"DD}
\DeclareMathSymbol{\nleqslant}{3}{arrows}{"D6}
\DeclareMathSymbol{\ngeqslant}{3}{arrows}{"D7}
\DeclareMathSymbol{\lneq}{3}{arrows}{"DA}
\DeclareMathSymbol{\gneq}{3}{arrows}{"DB}
\DeclareMathSymbol{\npreceq}{3}{arrows}{"E7}
\DeclareMathSymbol{\nsucceq}{3}{arrows}{"E8}
\DeclareMathSymbol{\precnsim}{3}{arrows}{"EB}
\DeclareMathSymbol{\succnsim}{3}{arrows}{"EC}
\DeclareMathSymbol{\lnsim}{3}{arrows}{"E0}
\DeclareMathSymbol{\gnsim}{3}{arrows}{"E2}
\DeclareMathSymbol{\nleqq}{3}{arrows}{"D8}
\DeclareMathSymbol{\ngeqq}{3}{arrows}{"D9}
\DeclareMathSymbol{\precneqq}{3}{arrows}{"E9}
\DeclareMathSymbol{\succneqq}{3}{arrows}{"EA}
\DeclareMathSymbol{\precnapprox}{3}{arrows}{"ED}
\DeclareMathSymbol{\succnapprox}{3}{arrows}{"EE}
\DeclareMathSymbol{\lnapprox}{3}{arrows}{"E3}
\DeclareMathSymbol{\gnapprox}{3}{arrows}{"E4}
\DeclareMathSymbol{\nsim}{3}{arrows}{"96}
\DeclareMathSymbol{\ncong}{3}{arrows}{"99}
\DeclareMathSymbol{\diagup}{3}{arrows}{"0B}
\DeclareMathSymbol{\diagdown}{3}{arrows}{"0C}
\DeclareMathSymbol{\varsubsetneq}{3}{arrows}{"D0}
\DeclareMathSymbol{\varsupsetneq}{3}{arrows}{"D1}
\DeclareMathSymbol{\nsubseteqq}{3}{arrows}{"CA}
\DeclareMathSymbol{\nsupseteqq}{3}{arrows}{"CB}
\DeclareMathSymbol{\subsetneqq}{3}{arrows}{"CE}
\DeclareMathSymbol{\supsetneqq}{3}{arrows}{"CF}
\DeclareMathSymbol{\varsubsetneqq}{3}{arrows}{"D2}
\DeclareMathSymbol{\varsupsetneqq}{3}{arrows}{"D3}
\DeclareMathSymbol{\subsetneq}{3}{arrows}{"CC}
\DeclareMathSymbol{\supsetneq}{3}{arrows}{"CD}
\DeclareMathSymbol{\nsubseteq}{3}{arrows}{"C8}
\DeclareMathSymbol{\nsupseteq}{3}{arrows}{"C9}
\DeclareMathSymbol{\nparallel}{3}{arrows}{"F7}
\DeclareMathSymbol{\nmid}{3}{arrows}{"F6}
\DeclareMathSymbol{\nshortmid}{3}{arrows}{"F4}
\DeclareMathSymbol{\nshortparallel}{3}{arrows}{"F5}
\DeclareMathSymbol{\nvdash}{3}{arrows}{"F8}
\DeclareMathSymbol{\nVdash}{3}{arrows}{"FA}
\DeclareMathSymbol{\nvDash}{3}{arrows}{"F9}
\DeclareMathSymbol{\nVDash}{3}{arrows}{"FB}
\DeclareMathSymbol{\ntrianglerighteq}{3}{arrows}{"F2}
\DeclareMathSymbol{\ntrianglelefteq}{3}{arrows}{"F1}
\DeclareMathSymbol{\ntriangleleft}{3}{arrows}{"EF}
\DeclareMathSymbol{\ntriangleright}{3}{arrows}{"F0}
\DeclareMathSymbol{\nleftarrow}{3}{arrows}{"32}
\DeclareMathSymbol{\nrightarrow}{3}{arrows}{"33}
\DeclareMathSymbol{\nLeftarrow}{3}{arrows}{"66}
\DeclareMathSymbol{\nRightarrow}{3}{arrows}{"68}
\DeclareMathSymbol{\nLeftrightarrow}{3}{arrows}{"67}
\DeclareMathSymbol{\nleftrightarrow}{3}{arrows}{"34}
\mathchardef\divideontimes="21F7
% \mathchardef\varnothing="023B
\mathchardef\varnothing="019C
\DeclareMathSymbol{\nexists}{0}{arrows}{"20}
\mathchardef\Finv="0190
\mathchardef\Game="0191
\mathchardef\mho="0192
\mathchardef\simeq="329A
\mathchardef\eqsim="3299
\mathchardef\beth="0195
\mathchardef\gimel="0196
\mathchardef\daleth="0197
\mathchardef\lessdot="31DC
\mathchardef\gtrdot="31DD
\mathchardef\ltimes="21CE
\mathchardef\rtimes="21CF
\mathchardef\shortmid="31F4
\mathchardef\shortparallel="31F5
\mathchardef\smallsetminus="21D8 % ?
\mathchardef\thicksim="3218 % ?
\mathchardef\thickapprox="3219 % ?	
\mathchardef\approxeq="329D
\mathchardef\succapprox="31ED
\mathchardef\precapprox="31EC
\DeclareMathSymbol{\curvearrowleft}{3}{arrows}{"87}
\DeclareMathSymbol{\curvearrowright}{3}{arrows}{"88}
\mathchardef\digamma="0146 % ?
\mathchardef\varkappa="019B
\DeclareMathSymbol{\Bbbk}{0}{arrows}{"6B}
\mathchardef\hslash="019D
\DeclareMathSymbol{\hbar}{0}{arrows}{"1B}
\mathchardef\backepsilon="31FB % ?

\DeclareMathSymbol{\dashrightarrow}{0}{arrows}{"3A}
\DeclareMathSymbol{\dashleftarrow}{0}{arrows}{"38}
\DeclareMathSymbol{\dashuparrow}{0}{arrows}{"39}
\DeclareMathSymbol{\dashdownarrow}{0}{arrows}{"3B}

\DeclareMathDelimiter\ulcorner{4}{arrows}{"70}{arrows}{"70}
\DeclareMathDelimiter\urcorner{5}{arrows}{"71}{arrows}{"71}
\DeclareMathDelimiter\llcorner{4}{arrows}{"78}{arrows}{"78}
\DeclareMathDelimiter\lrcorner{5}{arrows}{"79}{arrows}{"79}

% Following only to define \mathhexbox for \checkmark, \circledR, \maltese


\expandafter\ifx\csname amstext.sty\endcsname\relax %MJD%
% %MJD% then amstext.sty not in use. OK to redefine \text.
  \def\RIfM@{\relax\ifmmode}
  \def\DN@{\def\next@}
  \def\eat@#1{}
  \newif\iffirstchoice@
  \firstchoice@true
  \def\text@#1{\mathchoice
   {\hbox{\everymath{\displaystyle}\def\textfonti{\the\textfont\@ne}%
    \def\textfontii{\the\textfont\tw@}\textdef@@ T#1}}
   {\hbox{\firstchoice@false
    \everymath{\textstyle}\def\textfonti{\the\textfont\@ne}%
    \def\textfontii{\the\textfont\tw@}\textdef@@ T#1}}
   {\hbox{\firstchoice@false
    \everymath{\scriptstyle}\def\textfonti{\the\scriptfont\@ne}%
    \def\textfontii{\the\scriptfont\tw@}\textdef@@ S\rm#1}}
   {\hbox{\firstchoice@false
    \everymath{\scriptscriptstyle}\def\textfonti
    {\the\scriptscriptfont\@ne}%
    \def\textfontii{\the\scriptscriptfont\tw@}\textdef@@ s\rm#1}}}
  \def\textdef@@#1{\textdef@#1\rm\textdef@#1\bf\textdef@#1\sl\textdef@#1\it}
  \def\text@@#1{\leavevmode\hbox{#1}}
  \def\rmfam{0}
  \def\textdef@#1#2{%
   \DN@{\csname\expandafter\eat@\string#2fam\endcsname}%
   \if S#1\edef#2{\the\scriptfont\next@\relax}%
   \else\if s#1\edef#2{\the\scriptscriptfont\next@\relax}%
   \else\edef#2{\the\textfont\next@\relax}\fi\fi}
  \def\text{\RIfM@\expandafter\text@\else\expandafter\text@@\fi}
  \def\mathhexbox@#1#2#3{\text{$\m@th\mathchar"#1#2#3$}}
\fi %MJD%

\xdef\checkmark{\noexpand\mathhexbox\hexnumber@\symarrows 58 }

\def\lmathhexbox#1#2#3{\leavevmode
  \hbox{$\m@th \mathchar"#1#2#3$}}
\def \circledR	{\lmathhexbox1C9 }
\def \maltese	{\lmathhexbox1CB }
% Note that plain TeX has the accent character positions hardwired to:

% 16 for `dotlessi', 17 for `dotlessj', 
% 18 for `grave', 19 for `acute', 20 for `caron', 
% 21 for `breve', 22 for `macron', 
% 23 for `ring', 24 for `cedilla',
% 25 for `germandbls', 26 for `ae', 27 for `oe', 
% 28 for `oslash', 29 for `AE', 30 for 'OE', 31 for `Oslash',
% 94 for `circumflex', 95 for `dotaccent', 125 for `hungarumlaut',
% 126 for `tilde', 127 for `dieresis',
% (see page 356 of the TeX book, and plain.tex for additional information)

% These may need to be adjusted - if these characters are to be used -
% AND if the text fonts are encoded to something other than TeX text.
% For an example of how to do this, see the file accents.tex.

% changes to lplain. i dont like 22C, so:
\let\Leftrightarrow\undefined
\DeclareMathSymbol{\Leftrightarrow}{3}{arrows}{"61}
%</lucidabright>
%
%    \end{macrocode}
% \Finale
\endinput