From cbbdf233cc4b0a07296302066e6feb323dcbdf72 Mon Sep 17 00:00:00 2001 From: Karl Berry Date: Fri, 13 Jan 2006 00:01:07 +0000 Subject: objectz git-svn-id: svn://tug.org/texlive/trunk@1151 c570f23f-e606-0410-a88d-b1316a301751 --- Master/texmf-dist/tex/latex/objectz/oz.sty | 964 +++++++++++++++++++++++++++++ 1 file changed, 964 insertions(+) create mode 100644 Master/texmf-dist/tex/latex/objectz/oz.sty (limited to 'Master') diff --git a/Master/texmf-dist/tex/latex/objectz/oz.sty b/Master/texmf-dist/tex/latex/objectz/oz.sty new file mode 100644 index 00000000000..251d45ca81e --- /dev/null +++ b/Master/texmf-dist/tex/latex/objectz/oz.sty @@ -0,0 +1,964 @@ +%% +%% This is file `oz.sty', +%% generated with the docstrip utility. +%% +%% The original source files were: +%% +%% oz.dtx (with options: `package') +%% Copyright (C) 1993 Sebastian Rahtz. All rights reserved. +%% This is a generated file for Object Z. Permission is granted to to +%% customize the declarations in this file to serve the needs of your +%% installation. However, no permission is granted to distribute a +%% modified version of this file under its original name. +%% +\def\fileversion{2.46} +\def\filedate{1999/05/24} +\def\docdate {1994/08/13} +%% File: oz.dtx Copyright (C) 1995-1999 Sebastian Rahtz +\NeedsTeXFormat{LaTeX2e}[1994/12/01] +\ProvidesPackage{oz}[\filedate\space\fileversion\space Object Z macros] +\message{`Object-Z Macros' \fileversion\space <\filedate>} +\RequirePackage{calc} +\def\oz@parbox{\@ifnextchar [{\oz@iparbox}{\oz@iparbox[c]}} +\long\def\oz@iparbox[#1]#2#3{\leavevmode \@pboxswfalse + \if #1b\vbox + \else \if #1t\vtop + \else \vbox + %\ifmmode \vcenter \else \@pboxswtrue $\vcenter \fi + \fi + \fi +{\hsize #2\@parboxrestore #3} + %\if@pboxsw \m@th$\fi +} +\@ifpackageloaded{lucbr}{}{% +\DeclareMathVersion{oz} +\SetMathAlphabet{\mathrm}{oz}{\encodingdefault}{\rmdefault}{m}{n}% +\SetMathAlphabet{\mathbf}{oz}{\encodingdefault}{\rmdefault}{bx}{n}% +\SetMathAlphabet{\mathsf}{oz}{\encodingdefault}{\sfdefault}{m}{n}% +\DeclareSymbolFont{italics}{\encodingdefault}{\rmdefault}{m}{it}% +\DeclareSymbolFontAlphabet{\mathrm}{operators} +\DeclareSymbolFontAlphabet{\mathit}{letters} +\DeclareSymbolFontAlphabet{\mathcal}{symbols} +\DeclareSymbolFontAlphabet{\ozit}{italics} +\DeclareSymbolFont{lasy}{U}{lasy}{m}{n} +\DeclareSymbolFont{AMSa}{U}{msa}{m}{n} +\DeclareSymbolFont{AMSb}{U}{msb}{m}{n} +\let\mho\undefined +\let\Join\undefined +\let\Box\undefined +\let\Diamond\undefined +\let\leadsto\undefined +\let\sqsubset\undefined +\let\sqsupset\undefined +\let\lhd\undefined +\let\unlhd\undefined +\let\rhd\undefined +\let\unrhd\undefined +\DeclareMathSymbol{\mho}{\mathord}{lasy}{"30} +\DeclareMathSymbol{\Join}{\mathrel}{lasy}{"31} +\DeclareMathSymbol{\Box}{\mathord}{lasy}{"32} +\DeclareMathSymbol{\Diamond}{\mathord}{lasy}{"33} +\DeclareMathSymbol{\leadsto}{\mathrel}{lasy}{"3B} +\DeclareMathSymbol{\sqsubset}{\mathrel}{lasy}{"3C} +\DeclareMathSymbol{\sqsupset}{\mathrel}{lasy}{"3D} +\DeclareMathSymbol{\lhd}{\mathrel}{lasy}{"01} +\DeclareMathSymbol{\unlhd}{\mathrel}{lasy}{"02} +\DeclareMathSymbol{\rhd}{\mathrel}{lasy}{"03} +\DeclareMathSymbol{\unrhd}{\mathrel}{lasy}{"04} +\DeclareSymbolFontAlphabet{\mathbb}{AMSb} +\DeclareSymbolFontAlphabet{\bbold}{AMSb} +\mathversion{oz} +} +\newbox\strutbox@ +\def\strut@{\copy\strutbox@} +\addto@hook\every@math@size{% + \setbox\strutbox@\hbox{\lower.5\normallineskiplimit + \vbox{\kern-\normallineskiplimit\copy\strutbox}}} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% NOTE: bBigg is used to define the font size for zbig etc +%% however it defines these as fixed sizes. +%% The 209 definitions set the font size dependent on the +%% current point size. +%% +%% Hence in 209 you can do \Large\cnj and the symbol is bigger +%% But in 2e it remains a fixed size! +%% +%% This is a problem for the Object-Z operators as originally +%% defined in the 209 oz.sty `96 file. +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\def\bBigg@#1#2{% +\mbox{\ifcase#1\or\large\or\Large\or\LARGE\or\small\or\footnotesize\fi +$#2$}\nulldelimiterspace\z@ \m@th} +\addto@hook\every@math@size{\setbox\z@\vbox{\hbox{$($}\kern\z@}% + \big@size 1.2\ht\z@} +\newdimen\big@size +\def\zBIG{\bBigg@{3}} +\def\zBig{\bBigg@{2}} +\def\zbig{\bBigg@{1}} +\def\zsmall{\bBigg@{4}} +\def\zSmall{\bBigg@{5}} +\def\String#1{\hbox{`\texttt{#1}'}} +\def\STRING#1{\hbox{``\texttt{#1}''}} +\def\infix#1{\z@rel{{\underline{#1}}}} +\def\word#1{\z@op{#1}} +\def\keyword#1{\z@op{\mbox{\textrm{#1}}}} +\def\boldword#1{\z@op{\mbox{\textbf{#1}}}} +\def\underword#1{\z@op{{\underline{#1}}}} +\def\underkeyword#1{\z@op{{\underline{\mbox{\textrm{#1}}}}}} +\def\underboldword#1{\z@op{{\underline{\mbox{\textbf{#1}}}}}} +\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}{"7\hexnumber@\symitalics41} +\@setmcodes{`a}{`z}{"7\hexnumber@\symitalics61} +\let\@mc=\mathchardef +\mathcode`\;="8000 % Makes ; active in math mode +{\catcode`\;=\active \gdef;{\semicolon\;}} +\@mc\semicolon="603B +\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}}} +\def\_{\leavevmode \vbox{\hrule width0.4em}} +\let\xforall=\forall +\let\xexists=\exists +\let\xlambda=\lambda +\let\xmu=\mu +\let\xsucc\succ +\let\xprec\prec +\let\dotaccent=\dot +\let\sectionsymbol=\S +\let\integral=\int +\let\product\prod +\def\p#1{\mathrel{\ooalign{\hfil$\mapstochar\mkern 5mu$\hfil\cr$#1$}}} +\def\f#1{\mathrel{\ooalign{\hfil + $\mapstochar\mkern 3mu\mapstochar\mkern 5mu$\hfil\cr$#1$}}} +\@ifpackageloaded{lucbr}{% + \DeclareMathSymbol{\doublebarwedge}{\mathbin}{symbols}{"D4} + \DeclareMathSymbol{\lll}{\mathrel}{letters}{"DE} + \DeclareMathSymbol{\ggg}{\mathrel}{letters}{"DF} + \DeclareMathSymbol{\eth}{\mathrel}{operators}{"F0} +}{% +\let\rightleftharpoons\undefined +\let\angle\undefined +\DeclareMathSymbol\boxdot{\mathbin}{AMSa}{"00} +\DeclareMathSymbol\boxplus{\mathbin}{AMSa}{"01} +\DeclareMathSymbol\boxtimes{\mathbin}{AMSa}{"02} +\DeclareMathSymbol\square{\mathord}{AMSa}{"03} +\DeclareMathSymbol\blacksquare{\mathord}{AMSa}{"04} +\DeclareMathSymbol\centerdot{\mathbin}{AMSa}{"05} +\DeclareMathSymbol\lozenge{\mathord}{AMSa}{"06} +\DeclareMathSymbol\blacklozenge{\mathord}{AMSa}{"07} +\DeclareMathSymbol\circlearrowright{\mathrel}{AMSa}{"08} +\DeclareMathSymbol\circlearrowleft{\mathrel}{AMSa}{"09} +\DeclareMathSymbol\rightleftharpoons{\mathrel}{AMSa}{"0A} +\DeclareMathSymbol\leftrightharpoons{\mathrel}{AMSa}{"0B} +\DeclareMathSymbol\boxminus{\mathbin}{AMSa}{"0C} +\DeclareMathSymbol\Vdash{\mathrel}{AMSa}{"0D} +\DeclareMathSymbol\Vvdash{\mathrel}{AMSa}{"0E} +\DeclareMathSymbol\vDash{\mathrel}{AMSa}{"0F} +\DeclareMathSymbol\twoheadrightarrow{\mathrel}{AMSa}{"10} +\DeclareMathSymbol\twoheadleftarrow{\mathrel}{AMSa}{"11} +\DeclareMathSymbol\leftleftarrows{\mathrel}{AMSa}{"12} +\DeclareMathSymbol\rightrightarrows{\mathrel}{AMSa}{"13} +\DeclareMathSymbol\upuparrows{\mathrel}{AMSa}{"14} +\DeclareMathSymbol\downdownarrows{\mathrel}{AMSa}{"15} +\DeclareMathSymbol\upharpoonright{\mathrel}{AMSa}{"16} +\DeclareMathSymbol\downharpoonright{\mathrel}{AMSa}{"17} +\DeclareMathSymbol\upharpoonleft{\mathrel}{AMSa}{"18} +\DeclareMathSymbol\downharpoonleft{\mathrel}{AMSa}{"19} +\DeclareMathSymbol\rightarrowtail{\mathrel}{AMSa}{"1A} +\DeclareMathSymbol\leftarrowtail{\mathrel}{AMSa}{"1B} +\DeclareMathSymbol\leftrightarrows{\mathrel}{AMSa}{"1C} +\DeclareMathSymbol\rightleftarrows{\mathrel}{AMSa}{"1D} +\DeclareMathSymbol\Lsh{\mathrel}{AMSa}{"1E} +\DeclareMathSymbol\Rsh{\mathrel}{AMSa}{"1F} +\DeclareMathSymbol\rightsquigarrow{\mathrel}{AMSa}{"20} +\DeclareMathSymbol\leftrightsquigarrow{\mathrel}{AMSa}{"21} +\DeclareMathSymbol\looparrowleft{\mathrel}{AMSa}{"22} +\DeclareMathSymbol\looparrowright{\mathrel}{AMSa}{"23} +\DeclareMathSymbol\circeq{\mathrel}{AMSa}{"24} +\DeclareMathSymbol\succsim{\mathrel}{AMSa}{"25} +\DeclareMathSymbol\gtrsim{\mathrel}{AMSa}{"26} +\DeclareMathSymbol\gtrapprox{\mathrel}{AMSa}{"27} +\DeclareMathSymbol\multimap{\mathrel}{AMSa}{"28} +\DeclareMathSymbol\therefore{\mathrel}{AMSa}{"29} +\DeclareMathSymbol\because{\mathrel}{AMSa}{"2A} +\DeclareMathSymbol\doteqdot{\mathrel}{AMSa}{"2B} +\DeclareMathSymbol\triangleq{\mathrel}{AMSa}{"2C} +\DeclareMathSymbol\precsim{\mathrel}{AMSa}{"2D} +\DeclareMathSymbol\lesssim{\mathrel}{AMSa}{"2E} +\DeclareMathSymbol\lessapprox{\mathrel}{AMSa}{"2F} +\DeclareMathSymbol\eqslantless{\mathrel}{AMSa}{"30} +\DeclareMathSymbol\eqslantgtr{\mathrel}{AMSa}{"31} +\DeclareMathSymbol\curlyeqprec{\mathrel}{AMSa}{"32} +\DeclareMathSymbol\curlyeqsucc{\mathrel}{AMSa}{"33} +\DeclareMathSymbol\preccurlyeq{\mathrel}{AMSa}{"34} +\DeclareMathSymbol\leqq{\mathrel}{AMSa}{"35} +\DeclareMathSymbol\leqslant{\mathrel}{AMSa}{"36} +\DeclareMathSymbol\lessgtr{\mathrel}{AMSa}{"37} +\DeclareMathSymbol\backprime{\mathord}{AMSa}{"38} +\DeclareMathSymbol\risingdotseq{\mathrel}{AMSa}{"3A} +\DeclareMathSymbol\fallingdotseq{\mathrel}{AMSa}{"3B} +\DeclareMathSymbol\succcurlyeq{\mathrel}{AMSa}{"3C} +\DeclareMathSymbol\geqq{\mathrel}{AMSa}{"3D} +\DeclareMathSymbol\geqslant{\mathrel}{AMSa}{"3E} +\DeclareMathSymbol\gtrless{\mathrel}{AMSa}{"3F} +\DeclareMathSymbol\sqsubset{\mathrel}{AMSa}{"40} +\DeclareMathSymbol\sqsupset{\mathrel}{AMSa}{"41} +\DeclareMathSymbol\vartriangleright{\mathrel}{AMSa}{"42} +\DeclareMathSymbol\vartriangleleft{\mathrel}{AMSa}{"43} +\DeclareMathSymbol\trianglerighteq{\mathrel}{AMSa}{"44} +\DeclareMathSymbol\trianglelefteq{\mathrel}{AMSa}{"45} +\DeclareMathSymbol\bigstar{\mathord}{AMSa}{"46} +\DeclareMathSymbol\between{\mathrel}{AMSa}{"47} +\DeclareMathSymbol\blacktriangledown{\mathord}{AMSa}{"48} +\DeclareMathSymbol\blacktriangleright{\mathrel}{AMSa}{"49} +\DeclareMathSymbol\blacktriangleleft{\mathrel}{AMSa}{"4A} +\DeclareMathSymbol\vartriangle{\mathord}{AMSa}{"4D} +\DeclareMathSymbol\blacktriangle{\mathord}{AMSa}{"4E} +\DeclareMathSymbol\triangledown{\mathord}{AMSa}{"4F} +\DeclareMathSymbol\eqcirc{\mathrel}{AMSa}{"50} +\DeclareMathSymbol\lesseqgtr{\mathrel}{AMSa}{"51} +\DeclareMathSymbol\gtreqless{\mathrel}{AMSa}{"52} +\DeclareMathSymbol\lesseqqgtr{\mathrel}{AMSa}{"53} +\DeclareMathSymbol\gtreqqless{\mathrel}{AMSa}{"54} +\DeclareMathSymbol\Rrightarrow{\mathrel}{AMSa}{"56} +\DeclareMathSymbol\Lleftarrow{\mathrel}{AMSa}{"57} +\DeclareMathSymbol\veebar{\mathbin}{AMSa}{"59} +\DeclareMathSymbol\barwedge{\mathbin}{AMSa}{"5A} +\DeclareMathSymbol\doublebarwedge{\mathbin}{AMSa}{"5B} +\DeclareMathSymbol\angle{\mathord}{AMSa}{"5C} +\DeclareMathSymbol\measuredangle{\mathord}{AMSa}{"5D} +\DeclareMathSymbol\sphericalangle{\mathord}{AMSa}{"5E} +\DeclareMathSymbol\varpropto{\mathrel}{AMSa}{"5F} +\DeclareMathSymbol\smallsmile{\mathrel}{AMSa}{"60} +\DeclareMathSymbol\smallfrown{\mathrel}{AMSa}{"61} +\DeclareMathSymbol\Subset{\mathrel}{AMSa}{"62} +\DeclareMathSymbol\Supset{\mathrel}{AMSa}{"63} +\DeclareMathSymbol\Cup{\mathbin}{AMSa}{"64} +\DeclareMathSymbol\Cap{\mathbin}{AMSa}{"65} +\DeclareMathSymbol\curlywedge{\mathbin}{AMSa}{"66} +\DeclareMathSymbol\curlyvee{\mathbin}{AMSa}{"67} +\DeclareMathSymbol\leftthreetimes{\mathbin}{AMSa}{"68} +\DeclareMathSymbol\rightthreetimes{\mathbin}{AMSa}{"69} +\DeclareMathSymbol\subseteqq{\mathrel}{AMSa}{"6A} +\DeclareMathSymbol\supseteqq{\mathrel}{AMSa}{"6B} +\DeclareMathSymbol\bumpeq{\mathrel}{AMSa}{"6C} +\DeclareMathSymbol\Bumpeq{\mathrel}{AMSa}{"6D} +\DeclareMathSymbol\lll{\mathrel}{AMSa}{"6E} +\DeclareMathSymbol\ggg{\mathrel}{AMSa}{"6F} +\DeclareMathDelimiter\ulcorner{4}{AMSa}{"70}{AMSa}{"70} +\DeclareMathDelimiter\urcorner{5}{AMSa}{"71}{AMSa}{"71} +\DeclareMathDelimiter\llcorner{4}{AMSa}{"78}{AMSa}{"78} +\DeclareMathDelimiter\lrcorner{5}{AMSa}{"79}{AMSa}{"79} +\xdef\yen {\noexpand\mathhexbox\hexnumber@\symAMSa 55 } +\xdef\checkmark{\noexpand\mathhexbox\hexnumber@\symAMSa 58 } +\xdef\circledR {\noexpand\mathhexbox\hexnumber@\symAMSa 72 } +\xdef\maltese {\noexpand\mathhexbox\hexnumber@\symAMSa 7A } +\DeclareMathSymbol\circledS{\mathord}{AMSa}{"73} +\DeclareMathSymbol\pitchfork{\mathrel}{AMSa}{"74} +\DeclareMathSymbol\dotplus{\mathbin}{AMSa}{"75} +\DeclareMathSymbol\backsim{\mathrel}{AMSa}{"76} +\DeclareMathSymbol\backsimeq{\mathrel}{AMSa}{"77} +\DeclareMathSymbol\complement{\mathord}{AMSa}{"7B} +\DeclareMathSymbol\intercal{\mathbin}{AMSa}{"7C} +\DeclareMathSymbol\circledcirc{\mathbin}{AMSa}{"7D} +\DeclareMathSymbol\circledast{\mathbin}{AMSa}{"7E} +\DeclareMathSymbol\circleddash{\mathbin}{AMSa}{"7F} +\DeclareMathSymbol\lvertneqq{\mathrel}{AMSb}{"00} +\DeclareMathSymbol\gvertneqq{\mathrel}{AMSb}{"01} +\DeclareMathSymbol\nleq{\mathrel}{AMSb}{"02} +\DeclareMathSymbol\ngeq{\mathrel}{AMSb}{"03} +\DeclareMathSymbol\nless{\mathrel}{AMSb}{"04} +\DeclareMathSymbol\ngtr{\mathrel}{AMSb}{"05} +\DeclareMathSymbol\nprec{\mathrel}{AMSb}{"06} +\DeclareMathSymbol\nsucc{\mathrel}{AMSb}{"07} +\DeclareMathSymbol\lneqq{\mathrel}{AMSb}{"08} +\DeclareMathSymbol\gneqq{\mathrel}{AMSb}{"09} +\DeclareMathSymbol\nleqslant{\mathrel}{AMSb}{"0A} +\DeclareMathSymbol\ngeqslant{\mathrel}{AMSb}{"0B} +\DeclareMathSymbol\lneq{\mathrel}{AMSb}{"0C} +\DeclareMathSymbol\gneq{\mathrel}{AMSb}{"0D} +\DeclareMathSymbol\npreceq{\mathrel}{AMSb}{"0E} +\DeclareMathSymbol\nsucceq{\mathrel}{AMSb}{"0F} +\DeclareMathSymbol\precnsim{\mathrel}{AMSb}{"10} +\DeclareMathSymbol\succnsim{\mathrel}{AMSb}{"11} +\DeclareMathSymbol\lnsim{\mathrel}{AMSb}{"12} +\DeclareMathSymbol\gnsim{\mathrel}{AMSb}{"13} +\DeclareMathSymbol\nleqq{\mathrel}{AMSb}{"14} +\DeclareMathSymbol\ngeqq{\mathrel}{AMSb}{"15} +\DeclareMathSymbol\precneqq{\mathrel}{AMSb}{"16} +\DeclareMathSymbol\succneqq{\mathrel}{AMSb}{"17} +\DeclareMathSymbol\precnapprox{\mathrel}{AMSb}{"18} +\DeclareMathSymbol\succnapprox{\mathrel}{AMSb}{"19} +\DeclareMathSymbol\lnapprox{\mathrel}{AMSb}{"1A} +\DeclareMathSymbol\gnapprox{\mathrel}{AMSb}{"1B} +\DeclareMathSymbol\nsim{\mathrel}{AMSb}{"1C} +\DeclareMathSymbol\ncong{\mathrel}{AMSb}{"1D} +\DeclareMathSymbol\nsubseteqq{\mathrel}{AMSb}{"22} +\DeclareMathSymbol\nsupseteqq{\mathrel}{AMSb}{"23} +\DeclareMathSymbol\subsetneqq{\mathrel}{AMSb}{"24} +\DeclareMathSymbol\supsetneqq{\mathrel}{AMSb}{"25} +\DeclareMathSymbol\subsetneq{\mathrel}{AMSb}{"28} +\DeclareMathSymbol\supsetneq{\mathrel}{AMSb}{"29} +\DeclareMathSymbol\nsubseteq{\mathrel}{AMSb}{"2A} +\DeclareMathSymbol\nsupseteq{\mathrel}{AMSb}{"2B} +\DeclareMathSymbol\nparallel{\mathrel}{AMSb}{"2C} +\DeclareMathSymbol\nmid{\mathrel}{AMSb}{"2D} +\DeclareMathSymbol\nshortmid{\mathrel}{AMSb}{"2E} +\DeclareMathSymbol\nshortparallel{\mathrel}{AMSb}{"2F} +\DeclareMathSymbol\nvdash{\mathrel}{AMSb}{"30} +\DeclareMathSymbol\nVdash{\mathrel}{AMSb}{"31} +\DeclareMathSymbol\nvDash{\mathrel}{AMSb}{"32} +\DeclareMathSymbol\nVDash{\mathrel}{AMSb}{"33} +\DeclareMathSymbol\ntrianglerighteq{\mathrel}{AMSb}{"34} +\DeclareMathSymbol\ntrianglelefteq{\mathrel}{AMSb}{"35} +\DeclareMathSymbol\ntriangleleft{\mathrel}{AMSb}{"36} +\DeclareMathSymbol\ntriangleright{\mathrel}{AMSb}{"37} +\DeclareMathSymbol\nleftarrow{\mathrel}{AMSb}{"38} +\DeclareMathSymbol\nrightarrow{\mathrel}{AMSb}{"39} +\DeclareMathSymbol\nLeftarrow{\mathrel}{AMSb}{"3A} +\DeclareMathSymbol\nRightarrow{\mathrel}{AMSb}{"3B} +\DeclareMathSymbol\nLeftrightarrow{\mathrel}{AMSb}{"3C} +\DeclareMathSymbol\nleftrightarrow{\mathrel}{AMSb}{"3D} +\DeclareMathSymbol\divideontimes{\mathbin}{AMSb}{"3E} +\DeclareMathSymbol\varnothing{\mathord}{AMSb}{"3F} +\DeclareMathSymbol\mho{\mathord}{AMSb}{"66} +\DeclareMathSymbol\eth{\mathord}{AMSb}{"67} +\DeclareMathSymbol\eqsim{\mathrel}{AMSb}{"68} +\DeclareMathSymbol\beth{\mathord}{AMSb}{"69} +\DeclareMathSymbol\gimel{\mathord}{AMSb}{"6A} +\DeclareMathSymbol\daleth{\mathord}{AMSb}{"6B} +\DeclareMathSymbol\lessdot{\mathrel}{AMSb}{"6C} +\DeclareMathSymbol\gtrdot{\mathrel}{AMSb}{"6D} +\DeclareMathSymbol\ltimes{\mathbin}{AMSb}{"6E} +\DeclareMathSymbol\rtimes{\mathbin}{AMSb}{"6F} +\DeclareMathSymbol\shortmid{\mathrel}{AMSb}{"70} +\DeclareMathSymbol\shortparallel{\mathrel}{AMSb}{"71} +\DeclareMathSymbol\smallsetminus{\mathbin}{AMSb}{"72} +\DeclareMathSymbol\thicksim{\mathrel}{AMSb}{"73} +\DeclareMathSymbol\thickapprox{\mathrel}{AMSb}{"74} +\DeclareMathSymbol\approxeq{\mathrel}{AMSb}{"75} +\DeclareMathSymbol\succapprox{\mathrel}{AMSb}{"76} +\DeclareMathSymbol\precapprox{\mathrel}{AMSb}{"77} +\DeclareMathSymbol\curvearrowleft{\mathrel}{AMSb}{"78} +\DeclareMathSymbol\curvearrowright{\mathrel}{AMSb}{"79} +\DeclareMathSymbol\digamma{\mathord}{AMSb}{"7A} +\DeclareMathSymbol\varkappa{\mathord}{AMSb}{"7B} +\DeclareMathSymbol\hslash{\mathord}{AMSb}{"7D} +\DeclareMathSymbol\hbar{\mathord}{AMSb}{"7E} +\DeclareMathSymbol\backepsilon{\mathrel}{AMSb}{"7F} +} +\def\interleave{{\parallel\!\!\vert}} +\def\shortinterleave{\z@rel{\mathord\shortmid\mathord\shortparallel}} +\def\napprox{\not\approx} +\let\restriction\upharpoonright +\let\Doteq\doteqdot +\let\doublecup\Cup +\let\llless\lll +\let\gggtr\ggg +\let\doublecap\Cap +\def \nat {{\mathbb N}} +\def \integer {{\mathbb Z}} +\def \natone {{\mathbb N}_1} +\def \real {{\mathbb R}} +\def \bool {{\mathbb B}} +\let \divides \div +\def \div {\z@bin{\mathrm{div}}} +\def \mod {\z@bin{\mathrm{mod}}} +\def \succ {\word{succ}} +\def \expon {^} +\let \num \integer +\let \nplus \natone +\def \lnot {\neg\;} +\def \land {\z@rel{\wedge}} +\def \lor {\z@rel{\vee}} +\let \imp \Rightarrow +\let\iff \Leftrightarrow +\def \all {\z@op{\xforall}} +\def \exi {\z@op{\xexists}} +\def \exione {\exists_1} +\@ifpackageloaded{lucbr}{% +\DeclareMathSymbol{\nexi}{0}{arrows}{"20} +}{% +\DeclareMathSymbol{\nexi}{\mathord}{AMSb}{"40} +} +\def \dot {\z@rel{\bullet}} +\def \true {\keyword{true}} +\def \false {\keyword{false}} +\let \cond \rightarrow +\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 +\let \emptyset \varnothing +\def \varemptyset {\{\,\}} +\def \pset {\z@op{\mathbb P}} +\def \psetone {\pset_1} +\def \fset {\z@op{\mathbb F}} +\def \fsetone {\fset_1} +\def \sset {\z@op{\mathbb S}} +\let \mem \in +\def \nem {\not\mem} +\def \uni {\z@bin\cup} +\def \int {\z@bin\cap} +\let \prod \times +\def \min {\word{min}} +\def \max {\word{max}} +\def \duni {\z@Bigop{\lower0.25ex\hbox{$\uni$}}} +\def \dint {\z@Bigop{\lower0.25ex\hbox{$\int$}}} +\def \upto {\z@bin{\ldotp\ldotp}} +\let \psubs \subset +\let \subs \subseteq +\let \psups \supset +\let \sups \supseteq +\def \diff {\z@bin{\backslash}} +\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 +\def \lambda {\z@op{\xlambda}} +\def \mu {\z@op{\xmu}} +\def \dom {\keyword{dom}} +\def \ran {\keyword{ran}} +\def \id {\keyword{id}} +\@ifpackageloaded{lucbr}{% +\DeclareMathSymbol{\dres}{\mathbin}{letters}{"2F} +\DeclareMathSymbol{\rres}{\mathbin}{letters}{"2E} +}{% +\DeclareMathSymbol{\dres}{\mathbin}{AMSa}{"43} +\DeclareMathSymbol{\rres}{\mathbin}{AMSa}{"42} +} +\def \dsub {\mathbin{\rlap{\raise.05ex\hbox{$-$}}{\dres}}} +\def \rsub {\mathbin{\rlap{\raise.05ex\hbox{$-$}}{\rres}}} +\let \fovr \oplus +\let \cmp \circ +\def \fcmp {\mathbin{\raise 0.6ex\hbox{\oalign{\hfil$\scriptscriptstyle + \mathrm{o}$\hfil\cr\hfil$\scriptscriptstyle\mathrm{9}$\hfil}}}} +\def \inv {^\sim} +\def \limg {(\!|} +\def \rimg {|\!)} +\let \map \mapsto +\let \rel \leftrightarrow +\let \tfun \rightarrow +\let \tinj \rightarrowtail +\def \tsur {\mathrel{\ooalign{$\tfun$\hfil\cr$\mkern4mu\tfun$}}} +\def \pfun {\p\tfun} +\def \pinj {\p\tinj} +\def \psur {\p\tsur} +\def \ffun {\f\tfun} +\def \finj {\f\tinj} +\def \bij {\mathrel{\ooalign{$\tinj$\hfil\cr$\mkern5mu\tfun$}}} +\def \tcl {^+} +\def \rtcl {^*} +\def \iter {^} +\let \comp \fcmp +\let \ndres \dsub +\let \nrres \rsub +\let \fun \tfun +\let \inj \tinj +\let \surj \tsur +\let \psurj \psur +\let \llless \lll +\let \gggtr \ggg +\def \interleave {{\parallel\!\!\vert}} +\def \shortinterleave {\z@rel{\mathord\shortmid\mathord\shortparallel}} +\let \restriction \upharpoonright +\def \napprox {\not\approx} +\def \seq {\keyword{seq}} +\def \iseq {\keyword{iseq}} +\def \seqone {\seq_1} +\def \emptyseq {\lseq\,\rseq} +\let \lseq \langle +\let \rseq \rangle +\def \head {\word{head}} +\def \tail {\word{tail}} +\def \front {\word{front}} +\def \last {\word{last}} +\def \rev {\word{rev}} +\def \squash {\word{squash}} +\def \next {\keyword{next}} +\def \inseq {\keyword{in}} +\@ifpackageloaded{lucbr}{% +\DeclareMathSymbol{\sres}{2}{arrows}{"75} +\DeclareMathSymbol{\ires}{2}{arrows}{"76} +\DeclareMathSymbol{\@@cat}{\mathbin}{operators}{"5F} +}{% +\DeclareMathSymbol{\@@cat}{\mathbin}{AMSa}{"61} +\DeclareMathSymbol{\sres}{\mathbin}{AMSa}{"16} +\DeclareMathSymbol{\ires}{\mathbin}{AMSa}{"18} +} +\def \cat {\mathbin{\raise 0.8ex\hbox{$\mathchar\@@cat$}}} +\def \ssub {\z@bin{\rlap{$-$}{\sres}}} +\def \isub {\z@bin{\rlap{$-$}{\ires}}} +\def \dcat {\z@op{\cat/}} +\def \dovr {\z@op{\fovr/}} +\def \dcmp {\z@op{\fcmp/}} +\let \prefix \subseteq +\def \suffix {\keyword{suffix}} +\def \seqi {\keyword{seq_\infty}} +\def \partitions {\keyword{partitions}} +\def \partition {\keyword{partitions}} +\def \disjoint {\keyword{disjoint}} +\def \subseq {\keyword{subseq}} +\let \filter \sres +\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]} +\let \project \zproject +\let \import \sres +\let \semi \zcmp +\let \hide \zhide +\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}} +\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} +\let \sdefs \sdef +\mathcode`\|=\mid +\let \ldata \lang +\let \rdata \rang +\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}} +\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} +\def\qua{\mbox{::}} +\def\redef{\mbox{\textbf{~redef}}} +\def\Init{I\!{\scriptstyle{NIT}}} +\def\Exit{E\!{\scriptstyle{XIT}}} +\def\Internal{I\!{\scriptstyle{NTERNAL}}} +\def\Aux{A\!{\scriptstyle{UX}}} +\def\intern{\mbox{\textsf{i}}} +\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$}}} +\let\shows\thrm +\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} +\let\inherits\childof +\let\subclass\childof +\let\isa\childof +\let\supclass\parentof +\let\instantiates\hasa +\let\islikea\weaksubclass +\def\poly{\mathord\downarrow} +\def\widen#1{\z@op{{\overline{#1}}}} +\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$}} +\let\henceforth\always +\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}]}} +\def \oid {{\bbold O}} +\def \self {\word{self}} +\def \contained {\word{contained}} +\let \classuni \uni +\def \visibility {\zproject} +\def \invisibility {{\project\hspace{-0.63 em}\cross}} +\def \cid {{\bigcirc\mbox{\scriptsize{\hspace{-0.78em}}\mbox{\tiny{C}}}}} +\def \sid {{\bigcirc\mbox{\scriptsize{\hspace{-0.74em}}\mbox{\tiny{S}}}}} +\def \eid {{\bigcirc\mbox{\scriptsize{\hspace{-0.74em}}\mbox{\tiny{E}}}}} +\def \pll {~\parallel~} +\def \plo {~\parallel_{!}~} +\def \sqc {~\semi~} +\def \cnj {~\zand~} +\def \gch {~[\mbox{\hspace{-0.06em}}]~} +\def \enh {~\dot~} +\def \dsqc {\mbox{{\Large $\fcmp~$}}} +\def \dgch {\mbox{{\Large $[\mbox{\hspace{-0.06em}}]$}}} +\def \dcnj {\mbox{{\Large $\land$}}} +\def \dpll {\mbox{{\Large $\parallel$}}} +\def \dplo {\mbox{{\Large $\parallel_{!}$}}} +\newcount\z@stackmin +\newcount\z@stackmax +\newcount\z@stacktop +\newdimen\@gtempa \z@stackmin=\allocationnumber +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa +\z@stackmax=\allocationnumber +\dimen\z@stackmin=0pt +\newbox\z@curline +\newdimen\z@curindent +\dimen\z@curindent=0pt +\def\z@space{{}\;{}} +\newbox\z@curfield +\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 +\newdimen\zedindent \zedindent=\leftmargini +\newdimen\zedleftsep \zedleftsep=1em +\newdimen\zedtab \zedtab=2em +\newdimen\zedbar \zedbar=8em +\newdimen\zedlinethickness \zedlinethickness=0.4pt +\newdimen\zedcornerheight \zedcornerheight=0pt +\newcount\z@cols +\newif\ifz@firstline \z@firstlinefalse +\newif\ifz@inclass \z@inclassfalse +\newif\ifz@inenv \z@inenvfalse +\newif\ifz@leftmargin \z@leftmargintrue +\newif\ifz@incols \z@incolsfalse +\newif\ifleftnames \leftnamesfalse +\def\leftschemas{\leftnamestrue} +\newif\ifz@inbox \z@inboxfalse +\newskip\zedbaselineskip \zedbaselineskip\baselineskip +\newbox\zstrutbox \setbox\zstrutbox=\copy\strutbox +\def\zstrut{\relax\ifmmode\copy\zstrutbox\else\unhcopy\zstrutbox\fi} +\def\zedbaselinestretch{1} +\def\baselinestretch{1} +\newcount\interzedlinepenalty \interzedlinepenalty=10000 %never break +\newcount\preboxpenalty \preboxpenalty=0 %break easily +\newcount\forcepagepenalty \forcepagepenalty=-10000 %always break +\interdisplaylinepenalty=100 %break sometimes +\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@} +\def\@setfontsize#1#2#3{\@nomath#1% + \ifx\protect\@typeset@protect + \let\@currsize#1% + \fi + \fontsize{#2}{#3}\selectfont +\setlength{\zedbaselineskip}{\baselineskip/\real{\baselinestretch}}% + \zedbaselineskip\zedbaselinestretch\zedbaselineskip + \setbox\zstrutbox\hbox{\vrule height.7\zedbaselineskip + depth.3\zedbaselineskip width\z@}} +\def\z@narrow{\advance\linewidth by -\zedindent} +\def\z@wide{\advance\linewidth by \zedindent} +\def\z@hrulefill{\leaders\hrule height\zedlinethickness\hfill} +\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 +\def\z@left{\ifz@inbox\vrule width\zedlinethickness\hskip\zedleftsep\fi} +\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 +} +\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} +\def\@but{\noalign{\nointerlineskip}} +\def\z@nopar{\global\@endpetrue} +\def\z@leavevmode{\ifvmode\if@inlabel\indent\else\if@noskipsec\indent\else + \if@nobreak\global\@nobreakfalse\everypar={}\fi + {\parskip=0pt\noindent}\fi\fi\fi} +\def\also{\crcr\noalign{\vskip\jot}} +\def\Also{\crcr\noalign{\vskip2\jot}} +\def\ALSO{\Also\Also} +\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} +\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\flushr#1{\crcr\quad\cr} +\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 \space to quit and then correct your document.} +\fi\fi} +\def\z@makeouter{% + \ifz@inenv + \ifz@inclass\z@inenvfalse + \hskip-\zedleftsep \advance\linewidth by -\zedlinethickness + \zedindent=\zedleftsep \zedleftsep=0.8\zedleftsep + \zedbar=0.8\zedbar \zedtab=0.8\zedtab + \oz@parbox{\linewidth}\bgroup + \z@zeroskips + \else + \@latexerr{Incorrect place for Z environment; nesting is + allowed only inside classes} + {You've either forgotten to finish the last environment,^^J% + you've forgotten to include a + \string\begin\string{class\string} somewhere^^J% + or you are trying to print a file that needs updating.^^J% + (Then again, you might just be trying to do something^^J% + that the author of these macros didn't intend you to do)^^J\@ehc} + \fi + \else + \bgroup + \fi +} +\def \z@makeinner{\egroup + \global\z@curindent\z@ +} +\def \classbreak{\also\egroup$$\vskip -\ht\zstrutbox + \vskip -\abovedisplayskip\vskip -\belowdisplayskip\z@wide\z@boxenv\also} +\def\zed{\z@outnonbox\z@inboxfalse\z@format} +\def\endzed{\crcr\egroup\endz@env} +\let\[=\zed +\def\]{\crcr\egroup$$\ignorespaces} +\def\argue{\z@outnonbox\interzedlinepenalty=\interdisplaylinepenalty + \openup 1\jot \z@format + \noalign{\vskip-\jot}}% equal vspace above and below argue display +\let\endargue=\endzed +\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} +\def\syntax{\z@outnonbox\halign\bgroup + \zstrut$\@lign##$\hfil &\hfil$\@lign{}##{}$\hfil + &$\@lign##$\hfil &\qquad\@lign-- ##\hfil\cr} +\let\endsyntax=\endzed +\def\schema#1{\z@inoutbox\z@topline{$\,#1\,$}} +\def\endschema{\z@botline \endzed \z@makeinner \z@nopar} +\@namedef{anonschema}{\leftnamesfalse\z@inoutbox\z@topline{}} +\expandafter\let\csname endanonschema\endcsname=\endschema +\def\genschema#1#2{\z@inoutbox\z@topline{$\,#1\:[#2]\,$}} +\let\endgenschema=\endschema +\def\axdef{\z@inoutbox} +\def\endaxdef{\endzed\z@makeinner} +\def\uniqdef{\leftnamesfalse\z@inoutbox\z@dbltopline{}} +\let\enduniqdef=\endschema +\def\gendef{\@ifnextchar[{\z@gendef}{\z@@gendef}} +\def\z@gendef[#1]{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,[#1]\,$}} +\def\z@@gendef#1{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,[#1]\,$}} +\let\endgendef=\endschema +\def\gengendef{\@ifnextchar[{\z@gengendef}{\z@@gengendef}} +\def\z@gengendef[#1]{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,#1\,$}} +\def\z@@gengendef#1{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,#1\,$}} +\let\endgengendef=\endschema +\def\class#1{\z@leavevmode\z@makeouter\z@inclasstrue + \z@boxenv\z@topline{$\,#1\,$}} +\let\endclass\endschema +\def\op{\z@inclasscheck\schema} +\let\endop\endschema +\def\state{\z@inclasscheck\anonschema} +\let\endstate\endschema +\def\init{\z@inclasscheck\schema{\Init}} +\let\endinit\endschema +\let\const\axdef +\let\endconst\endaxdef +\def\type{\z@inclasscheck} +\let\endtype\relax +\def\sidebyside{\@ifnextchar[{\z@columns}{\z@columns[2]}} +\def\z@columns[#1]{\z@leavevmode\z@cols#1 \z@makeouter\z@narrow% + $$\lineskip=0pt\z@incolstrue + \predisplaysize\maxdimen + \ifz@leftmargin\hskip-\zedindent\z@leftmarginfalse\fi + \setbox0=\hbox to \linewidth\bgroup\z@zeroskips% + \divide\zedbar by \z@cols \divide\zedleftsep by \z@cols + \divide\zedtab by \z@cols \divide\linewidth by \z@cols + \oz@parbox[t]{\linewidth}\bgroup\z@wide} +\def\nextside{\egroup\hss\oz@parbox[t]{\linewidth}\bgroup\z@wide} +\newdimen\z@temp +\def\endsidebyside{\egroup\egroup + \z@temp\ht0 \advance\z@temp by \dp0\advance\z@temp by-\dp\zstrutbox + \hbox{\raise\z@temp\box0}\endz@env\z@makeinner\z@nopar} +\def\zpar{\z@leavevmode + \ifz@inenv\z@inclasstrue\fi% fudge to let zpar in all boxes + \z@makeouter\z@changesize + \advance\linewidth by -\z@curindent + \advance\linewidth by -\wd\z@curline + \hskip-\wd\z@curline\advance\linewidth by -\zedindent$$ + \ifz@leftmargin\hskip-\zedindent\fi% adjustment for first column + \advance\displayindent by \zedindent + \advance\displaywidth by -\zedindent + \advance\displayindent by \z@curindent + \advance\displayindent by \wd\z@curline + \advance\displaywidth by -\z@curindent + \advance\displaywidth by -\wd\z@curline + \global\setbox\z@curline\hbox{} + \z@narrow\oz@parbox[b]{\linewidth}\bgroup\hfil\break} +\def\endzpar{\egroup$$\z@makeinner\z@nopar} +\def \classcom{\zpar\sf} +\let \endclasscom=\endzpar +\def\proof{\zpar$\PR$\zpar} +\def\endproof{\endzpar\endzpar} +\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}} +\def\fuzzcompatible{% +\let\defs\sdef +\let\empty\emptyset +} +\endinput +%% +%% End of file `oz.sty'. -- cgit v1.2.3