|
|
@@ -1,964 +0,0 @@
|
|
|
-%%
|
|
|
-%% 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 <return> \space to quit and then correct your document.}
|
|
|
-\fi\fi}
|
|
|
-\def\z@makeouter{%
|
|
|
- \ifz@inenv
|
|
|
- \ifz@inclass\z@inenvfalse
|
|
|
- \hskip-\zedleftsep \advance\linewidth by -\zedlinethickness
|
|
|
- \zedindent=\zedleftsep \zedleftsep=0.8\zedleftsep
|
|
|
- \zedbar=0.8\zedbar \zedtab=0.8\zedtab
|
|
|
- \oz@parbox{\linewidth}\bgroup
|
|
|
- \z@zeroskips
|
|
|
- \else
|
|
|
- \@latexerr{Incorrect place for Z environment; nesting is
|
|
|
- allowed only inside classes}
|
|
|
- {You've either forgotten to finish the last environment,^^J%
|
|
|
- you've forgotten to include a
|
|
|
- \string\begin\string{class\string} somewhere^^J%
|
|
|
- or you are trying to print a file that needs updating.^^J%
|
|
|
- (Then again, you might just be trying to do something^^J%
|
|
|
- that the author of these macros didn't intend you to do)^^J\@ehc}
|
|
|
- \fi
|
|
|
- \else
|
|
|
- \bgroup
|
|
|
- \fi
|
|
|
-}
|
|
|
-\def \z@makeinner{\egroup
|
|
|
- \global\z@curindent\z@
|
|
|
-}
|
|
|
-\def \classbreak{\also\egroup$$\vskip -\ht\zstrutbox
|
|
|
- \vskip -\abovedisplayskip\vskip -\belowdisplayskip\z@wide\z@boxenv\also}
|
|
|
-\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'.
|