From 86a936a7e685ba9a7a275027910409748b3c2acc Mon Sep 17 00:00:00 2001 From: Karl Berry Date: Wed, 11 Jan 2006 23:55:43 +0000 Subject: trunk/Master/texmf-dist/source/latex/objectz git-svn-id: svn://tug.org/texlive/trunk@422 c570f23f-e606-0410-a88d-b1316a301751 --- Master/texmf-dist/source/latex/objectz/catalog | 7 + Master/texmf-dist/source/latex/objectz/makefile | 6 + Master/texmf-dist/source/latex/objectz/manifest | 9 + Master/texmf-dist/source/latex/objectz/oz.dtx | 1613 +++++++++++++++++++++++ Master/texmf-dist/source/latex/objectz/oz.ins | 53 + Master/texmf-dist/source/latex/objectz/readme | 45 + 6 files changed, 1733 insertions(+) create mode 100644 Master/texmf-dist/source/latex/objectz/catalog create mode 100644 Master/texmf-dist/source/latex/objectz/makefile create mode 100644 Master/texmf-dist/source/latex/objectz/manifest create mode 100644 Master/texmf-dist/source/latex/objectz/oz.dtx create mode 100644 Master/texmf-dist/source/latex/objectz/oz.ins create mode 100644 Master/texmf-dist/source/latex/objectz/readme (limited to 'Master/texmf-dist/source/latex/objectz') diff --git a/Master/texmf-dist/source/latex/objectz/catalog b/Master/texmf-dist/source/latex/objectz/catalog new file mode 100644 index 00000000000..7edc81a9fc4 --- /dev/null +++ b/Master/texmf-dist/source/latex/objectz/catalog @@ -0,0 +1,7 @@ +Name: objectz +Problems-To: s.rahtz@elsevier.co.uk +Author: Sebastian Rahtz +Date: 199r/01/06 +Version: 2.42 +Description: LaTeX package for typesetting Object Z schemas + diff --git a/Master/texmf-dist/source/latex/objectz/makefile b/Master/texmf-dist/source/latex/objectz/makefile new file mode 100644 index 00000000000..edb8e0f58a2 --- /dev/null +++ b/Master/texmf-dist/source/latex/objectz/makefile @@ -0,0 +1,6 @@ +oz: + tex oz.ins + latex oz.dtx + +clean: + -rm *.aux *.toc *.sty *.dvi *.log *.tmp diff --git a/Master/texmf-dist/source/latex/objectz/manifest b/Master/texmf-dist/source/latex/objectz/manifest new file mode 100644 index 00000000000..e68ae4938e0 --- /dev/null +++ b/Master/texmf-dist/source/latex/objectz/manifest @@ -0,0 +1,9 @@ +total 112 +-rw-r--r-- 1 srahtz 191 Aug 6 10:27 catalog +-rw-r--r-- 1 srahtz 79 Aug 6 10:27 makefile +-rw-r--r-- 1 srahtz 0 Jan 7 11:49 manifest +-rw-r--r-- 1 srahtz 54861 Nov 22 11:12 oz.dtx +-rw-r--r-- 1 srahtz 1272 Aug 6 10:27 oz.ins +-rw-r--r-- 1 srahtz 41883 Aug 6 10:27 ozguide.tex +-rw-r--r-- 1 srahtz 10865 Aug 6 10:27 oztest.tex +-rw-r--r-- 1 srahtz 1763 Jan 7 11:45 readme diff --git a/Master/texmf-dist/source/latex/objectz/oz.dtx b/Master/texmf-dist/source/latex/objectz/oz.dtx new file mode 100644 index 00000000000..e272cf1572c --- /dev/null +++ b/Master/texmf-dist/source/latex/objectz/oz.dtx @@ -0,0 +1,1613 @@ +\def\fileversion{2.46} +\def\filedate{1999/05/24} +\def\docdate {1994/08/13} +% +% \iffalse +%% File: oz.dtx Copyright (C) 1995-1999 Sebastian Rahtz +% Permission is hereby granted, free of charge, to any person obtaining +% a copy of this software and associated documentation files (the +% ``Software''), to deal in the Software without restriction, including +% without limitation the rights to use, copy, modify, merge, publish, +% distribute, sublicense, and/or sell copies of the Software, and to +% permit persons to whom the Software is furnished to do so, subject to +% the following conditions: +% +% The above copyright notice and this permission notice shall be included +% in all copies or substantial portions of the Software. +% +% THE SOFTWARE IS PROVIDED ``AS IS'', WITHOUT WARRANTY OF ANY KIND, EXPRESS +% OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +% MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. +% IN NO EVENT SHALL SEBASTIAN RAHTZ BE LIABLE FOR ANY CLAIM, DAMAGES OR +% OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, +% ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR +% OTHER DEALINGS IN THE SOFTWARE. +% +%<*driver> +\documentclass{ltxdoc} +\begin{document} + \title{The \textsf{oz} package\thanks{This file + has version number \fileversion, last + revised \filedate.}} + \author{edited by Sebastian Rahtz\\S.Rahtz@elsevier.co.uk} + \date{\filedate} + \maketitle + \tableofcontents + \DocInput{oz.dtx} +\end{document} +% +% \fi +% \CheckSum{3387} +% +% \section{Introduction} +% +% This file provides macros to typeset Object Z schemas. +%\subsection{Modification History} +% +% The original zed.sty file was written by Mike Spivey. +% These macros have been extensively modified to +% include extra symbols and environments for Object-Z +% and now have little resemblence to the original macros. +% Mike Spivey has also extended his macros along +% different lines for Z --- the latest version of macros +% are called fuzz.sty and come with a syntax checker for Z. +% They can be purchased for a small fee from: +% \texttt{mike@prg.oxford.ac.uk} +% +% \begin{quote} +% \begin{tabular}{lp{.6\textwidth}} +% 87 &original zed.sty file --- Mike Spivey\\ +% 88 &modified to include extra symbols and environments --- +% Paul King\\ +% 88 &modified to include macros for UQ editor --- Ray Neucom\\ +% May 89 &modified to include object-oriented constructs --- PK\\ +% Jun 89 &modified to automatically change Z symbol size --- PK\\ +% 27 Jul 89 &removed spurious space from |\@setsize| --- PK\\ +% 3 Aug 89 &adjust style of equation number field --- PK\\ +% 24 Aug 89 &add optional field to topline and zedline for proofs --- +% PK\\ +% 15 Sep 89 &added extra qed symbols, updated classcom and comment --- +% PK\\ +% 25 Sep 89 &renamed z@[bB]ig to z[bB]ig and changed temporal symbols +% --- PK\\ +% 30 Sep 89 &added |\znewpage|, |\Infrule|, removed space above state +% box --- PK\\ +% 12 Mar 90 &changed |\@setsize| to work better for double-spaced text +% --- PK\\ +% 31 Mar 90 &added definition for @ and |\bool| and redefined `;' --- +% PK\\ +% 9 May 90 &changed |\sdef| to |\varsdef|, |\sdef| \& |\def|s to +% Spivey's latest --- PK\\ +% 27 May 90 &added |\c{n}{text}| --- a tab like |\t{n}| with text at +% left --- PK\\ +% 29 May 90 &added `corners' to boxes and |\zedcornerheight| --- PK\\ +% 11 Jul 90 &added |\rename*[y/x]| and |\zseq \zset| ..., changed |\zeq| +% |\zimp| --- PK\\ +% 2 Aug 90 &added subseq --- PK\\ +% 2 Aug 90 &added |\subseq|, |\iseq| - PK\\ +% \end{tabular} +% +% \begin{tabular}{lp{.6\textwidth}} +% 9 Nov 90 &changed |\M| to hopefully interact better with spacing --- +% PK\\ +% 18 Dec 90 &changed to new AMS 2.0 fonts - PK (with help from Adrian Lee)\\ +% 11 Feb 91 &added |\poly| |\widen| and modified |\gendef| - PK\\ +% 10 Apr 91 &added |\fuzzcompatible| - PK\\ +% 1 Apr 91 &added |\gengendef| - Steve Atkinson\\ +% 24 Feb 92 &changed to work with NFSS --- Sebastian Rahtz\\ +% 29 Dec 92 &changed to work with NFSS2 --- Sebastian Rahtz\\ +% 23 Dec 93 &checked for |\LaTeXe|\\ +% 6 Jan 94 &checked again for |\LaTeXe| with help of David Carlisle\\ +% 7 Apr 94 & checked again, bundle files added\\ +% 13 Aug 94 & removed hard-wired number of family for math letters\\ +% & removed definition of |\c| as it prevents cedilla from working\\ +% 22 Feb 95 & updated for AMSLaTeX 2.1 and Lucida compatibility\\ +% 30 Aug 96 &added Object-Z notations in Section 2A - SA\\ +% 17 Sep 97 &re-added |\zedbaselinestretch| -- David Leadbetter\\ +% 20 July 98 &|state| environment can be used in |sidebyside| \\ +% &changed to work with |slides| class -- DL\\ +% 4 Nov 98 & fixed |\zedbaselinestretch| -- DL\\ +% 17 Nov 98 & fixed |\Init|, etc -- DL\\ +% 24 May 99 & removed extra space output by |\fontsize| -- Ian Hayes and DL +% \end{tabular} +% \end{quote} +% +%\subsection{Known Problems} +% +%\begin{enumerate} +% \item |\bBigg| defines |\zBig|, etc as fixed font sizes - +% in the original oz.sty (for \LaTeX 2.09) these sizing commands change +% the font size relative to the current font size (so a |\zBig| +% in the scope of a |\large| is bigger than a |\zBig| +% in the scope of a |\normalsize|); +% \item |sidebyside| works very poorly with the |class| environment +% - indentation of operation schemas is wrong; +% \item the |calc| package is needed for |\zedbaselinestretch|. +%\end{enumerate} +% +% +%\subsection{The Object-Z Homepage} +% +% The Object-Z homepage (http://svrc.it.uq.edu.au/Object-Z/) contains: +% +% \begin{itemize} +% \item Papers and Tech-reports on Object-Z; +% \item {\bf wizard} - the Object-Z type checker. +% \end{itemize} +% +% \noindent Please post any updates that you may make to this file to the +% Formal Methods Group -- fmg@it.uq.edu.au +% +% +% +% \newpage +% +% \StopEventually{} +% +% \begin{macrocode} +%<*package> +\NeedsTeXFormat{LaTeX2e}[1994/12/01] +\ProvidesPackage{oz}[\filedate\space\fileversion\space Object Z macros] +\message{`Object-Z Macros' \fileversion\space <\filedate>} +\RequirePackage{calc} +% \end{macrocode} +% The \LaTeXe\ parbox code is much more complicated, so we get back +% a simpler world from \LaTeX 209. +% \begin{macrocode} +\def\oz@parbox{\@ifnextchar [{\oz@iparbox}{\oz@iparbox[c]}} +\long\def\oz@iparbox[#1]#2#3{\leavevmode \@pboxswfalse + \if #1b\vbox + \else \if #1t\vtop + \else \vbox + %\ifmmode \vcenter \else \@pboxswtrue $\vcenter \fi + \fi + \fi +{\hsize #2\@parboxrestore #3} + %\if@pboxsw \m@th$\fi +} +% \end{macrocode} +% +%\section{Z fonts} +% +% The AMS extra symbol fonts are loaded if we are not using Lucida New Math. +% Note: msam and msbm sometimes called euxm and euym respectively +% NOTE: the new AMSFONTS 2.0 call these fonts msam and msbm repectively +% (the fonts below need to be renamed if you want to use the new fonts) +% +% \begin{macrocode} +\@ifpackageloaded{lucbr}{}{% +\DeclareMathVersion{oz} +\SetMathAlphabet{\mathrm}{oz}{\encodingdefault}{\rmdefault}{m}{n}% +\SetMathAlphabet{\mathbf}{oz}{\encodingdefault}{\rmdefault}{bx}{n}% +\SetMathAlphabet{\mathsf}{oz}{\encodingdefault}{\sfdefault}{m}{n}% +\DeclareSymbolFont{italics}{\encodingdefault}{\rmdefault}{m}{it}% +\DeclareSymbolFontAlphabet{\mathrm}{operators} +\DeclareSymbolFontAlphabet{\mathit}{letters} +\DeclareSymbolFontAlphabet{\mathcal}{symbols} +\DeclareSymbolFontAlphabet{\ozit}{italics} +\DeclareSymbolFont{lasy}{U}{lasy}{m}{n} +\DeclareSymbolFont{AMSa}{U}{msa}{m}{n} +\DeclareSymbolFont{AMSb}{U}{msb}{m}{n} +\let\mho\undefined +\let\Join\undefined +\let\Box\undefined +\let\Diamond\undefined +\let\leadsto\undefined +\let\sqsubset\undefined +\let\sqsupset\undefined +\let\lhd\undefined +\let\unlhd\undefined +\let\rhd\undefined +\let\unrhd\undefined +\DeclareMathSymbol{\mho}{\mathord}{lasy}{"30} +\DeclareMathSymbol{\Join}{\mathrel}{lasy}{"31} +\DeclareMathSymbol{\Box}{\mathord}{lasy}{"32} +\DeclareMathSymbol{\Diamond}{\mathord}{lasy}{"33} +\DeclareMathSymbol{\leadsto}{\mathrel}{lasy}{"3B} +\DeclareMathSymbol{\sqsubset}{\mathrel}{lasy}{"3C} +\DeclareMathSymbol{\sqsupset}{\mathrel}{lasy}{"3D} +\DeclareMathSymbol{\lhd}{\mathrel}{lasy}{"01} +\DeclareMathSymbol{\unlhd}{\mathrel}{lasy}{"02} +\DeclareMathSymbol{\rhd}{\mathrel}{lasy}{"03} +\DeclareMathSymbol{\unrhd}{\mathrel}{lasy}{"04} +\DeclareSymbolFontAlphabet{\mathbb}{AMSb} +\DeclareSymbolFontAlphabet{\bbold}{AMSb} +\mathversion{oz} +} +% \end{macrocode} +% +% Allow change of size within schemas. This is a sod to get right; +% my principle (eventually!) was to go out of math temporarily, change +% size, go into an inner math, do the business, then get out of math +% and back to outer math. +% +% \begin{macrocode} +\newbox\strutbox@ +\def\strut@{\copy\strutbox@} +\addto@hook\every@math@size{% + \setbox\strutbox@\hbox{\lower.5\normallineskiplimit + \vbox{\kern-\normallineskiplimit\copy\strutbox}}} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% NOTE: bBigg is used to define the font size for zbig etc +%% however it defines these as fixed sizes. +%% The 209 definitions set the font size dependent on the +%% current point size. +%% +%% Hence in 209 you can do \Large\cnj and the symbol is bigger +%% But in 2e it remains a fixed size! +%% +%% This is a problem for the Object-Z operators as originally +%% defined in the 209 oz.sty `96 file. +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\def\bBigg@#1#2{% +\mbox{\ifcase#1\or\large\or\Large\or\LARGE\or\small\or\footnotesize\fi +$#2$}\nulldelimiterspace\z@ \m@th} +\addto@hook\every@math@size{\setbox\z@\vbox{\hbox{$($}\kern\z@}% + \big@size 1.2\ht\z@} +\newdimen\big@size +\def\zBIG{\bBigg@{3}} +\def\zBig{\bBigg@{2}} +\def\zbig{\bBigg@{1}} +\def\zsmall{\bBigg@{4}} +\def\zSmall{\bBigg@{5}} +% \end{macrocode} +% +% WORD STYLES +% these need handling a bit differently in NFSS from the original. +% +% \begin{macrocode} +\def\String#1{\hbox{`\texttt{#1}'}} +\def\STRING#1{\hbox{``\texttt{#1}''}} +\def\infix#1{\z@rel{{\underline{#1}}}} +\def\word#1{\z@op{#1}} +\def\keyword#1{\z@op{\mbox{\textrm{#1}}}} +\def\boldword#1{\z@op{\mbox{\textbf{#1}}}} +\def\underword#1{\z@op{{\underline{#1}}}} +\def\underkeyword#1{\z@op{{\underline{\mbox{\textrm{#1}}}}}} +\def\underboldword#1{\z@op{{\underline{\mbox{\textbf{#1}}}}}} +% \end{macrocode} +% +%\section{Z symbols} +% +% The mathcodes for the letters A, ..., Z, a, ..., z are changed to +% generate text italic rather than math italic by default. This makes +% multi-letter identifiers look better. The mathcode for character c +% is set to |"7000| (variable family) + |"400| (text italic) + |c|. +% +% \begin{macrocode} +\def\@setmcodes#1#2#3{{\count0=#1 \count1=#3 + \loop \global\mathcode\count0=\count1 \ifnum \count0<#2 + \advance\count0 by1 \advance\count1 by1 \repeat}} +% \end{macrocode} +% Use |\hexnumber@\symitalics| +% in case other families are loaded before. +% (from D. Roegel, July 13, 1994) +% \begin{macrocode} +\@setmcodes{`A}{`Z}{"7\hexnumber@\symitalics41} +\@setmcodes{`a}{`z}{"7\hexnumber@\symitalics61} +% \end{macrocode} +% +% Also, the mathcode for semicolon is set to |"8000|, so it behaves as an +% active character in math mode; it is defined to insert a thick space. +% |\semicolon| is a semicolon as an ordinary symbol. +% +% \begin{macrocode} +\let\@mc=\mathchardef +\mathcode`\;="8000 % Makes ; active in math mode +{\catcode`\;=\active \gdef;{\semicolon\;}} +\@mc\semicolon="603B +% \end{macrocode} +% +%\section{Utility macros for Z symbols} +%\begin{tabular}{ll} +% |\z@op |& makes a large math operator\\ +% |\z@rel|& makes a math relation\\ +% |\z@bin|& makes a binary operator\\ +%\end{tabular} +% +% Each use a mathstrut to defeat TeX's vertical adjustment. +% |\z@bigXXX| is a big version of symbol +% +% \begin{macrocode} +\def\z@op#1{\mathop{\mathstrut{#1}}\nolimits} +\def\z@bin#1{\mathbin{\mathstrut{#1}}} +\def\z@rel#1{\mathrel{\mathstrut{#1}}} +% +\def\z@bigop#1{\z@op{\zbig{#1}}} +\def\z@bigbin#1{\z@bin{\zbig{#1}}} +\def\z@bigrel#1{\z@rel{\zbig{#1}}} +% +\def\z@Bigop#1{\z@op{\zBig{#1}}} +\def\z@Bigbin#1{\z@bin{\zBig{#1}}} +\def\z@Bigrel#1{\z@rel{\zBig{#1}}} +% +\def\z@smallop#1{\z@op{\zsmall{#1}}} +\def\z@smallbin#1{\z@bin{\zsmall{#1}}} +\def\z@smallrel#1{\z@rel{\zsmall{#1}}} +% \end{macrocode} +% +% This underscore doesn't have the little kern --- you get an italic +% correction anyway in math mode. +% \begin{macrocode} +\def\_{\leavevmode \vbox{\hrule width0.4em}} +% \end{macrocode} +% Save |\q| as |\xq| for quantifiers q. +% \begin{macrocode} +\let\xforall=\forall +\let\xexists=\exists +\let\xlambda=\lambda +\let\xmu=\mu +% \end{macrocode} +% Save other symbols +% \begin{macrocode} +\let\xsucc\succ +\let\xprec\prec +\let\dotaccent=\dot +\let\sectionsymbol=\S +\let\integral=\int +\let\product\prod +% \end{macrocode} +% |\p| and |\f| make arrows with 1 and 2 crossings resp. +% \begin{macrocode} +\def\p#1{\mathrel{\ooalign{\hfil$\mapstochar\mkern 5mu$\hfil\cr$#1$}}} +\def\f#1{\mathrel{\ooalign{\hfil + $\mapstochar\mkern 3mu\mapstochar\mkern 5mu$\hfil\cr$#1$}}} +\@ifpackageloaded{lucbr}{% + \DeclareMathSymbol{\doublebarwedge}{\mathbin}{symbols}{"D4} + \DeclareMathSymbol{\lll}{\mathrel}{letters}{"DE} + \DeclareMathSymbol{\ggg}{\mathrel}{letters}{"DF} + \DeclareMathSymbol{\eth}{\mathrel}{operators}{"F0} +}{% +% \end{macrocode} +%\section{Amstex symbol definitions} +% +% Do these before Z symbols so that we can use them in our special symbols. +% AMSa font: +% \begin{macrocode} +\let\rightleftharpoons\undefined +\let\angle\undefined +\DeclareMathSymbol\boxdot{\mathbin}{AMSa}{"00} +\DeclareMathSymbol\boxplus{\mathbin}{AMSa}{"01} +\DeclareMathSymbol\boxtimes{\mathbin}{AMSa}{"02} +\DeclareMathSymbol\square{\mathord}{AMSa}{"03} +\DeclareMathSymbol\blacksquare{\mathord}{AMSa}{"04} +\DeclareMathSymbol\centerdot{\mathbin}{AMSa}{"05} +\DeclareMathSymbol\lozenge{\mathord}{AMSa}{"06} +\DeclareMathSymbol\blacklozenge{\mathord}{AMSa}{"07} +\DeclareMathSymbol\circlearrowright{\mathrel}{AMSa}{"08} +\DeclareMathSymbol\circlearrowleft{\mathrel}{AMSa}{"09} +\DeclareMathSymbol\rightleftharpoons{\mathrel}{AMSa}{"0A} +\DeclareMathSymbol\leftrightharpoons{\mathrel}{AMSa}{"0B} +\DeclareMathSymbol\boxminus{\mathbin}{AMSa}{"0C} +\DeclareMathSymbol\Vdash{\mathrel}{AMSa}{"0D} +\DeclareMathSymbol\Vvdash{\mathrel}{AMSa}{"0E} +\DeclareMathSymbol\vDash{\mathrel}{AMSa}{"0F} +\DeclareMathSymbol\twoheadrightarrow{\mathrel}{AMSa}{"10} +\DeclareMathSymbol\twoheadleftarrow{\mathrel}{AMSa}{"11} +\DeclareMathSymbol\leftleftarrows{\mathrel}{AMSa}{"12} +\DeclareMathSymbol\rightrightarrows{\mathrel}{AMSa}{"13} +\DeclareMathSymbol\upuparrows{\mathrel}{AMSa}{"14} +\DeclareMathSymbol\downdownarrows{\mathrel}{AMSa}{"15} +\DeclareMathSymbol\upharpoonright{\mathrel}{AMSa}{"16} +\DeclareMathSymbol\downharpoonright{\mathrel}{AMSa}{"17} +\DeclareMathSymbol\upharpoonleft{\mathrel}{AMSa}{"18} +\DeclareMathSymbol\downharpoonleft{\mathrel}{AMSa}{"19} +\DeclareMathSymbol\rightarrowtail{\mathrel}{AMSa}{"1A} +\DeclareMathSymbol\leftarrowtail{\mathrel}{AMSa}{"1B} +\DeclareMathSymbol\leftrightarrows{\mathrel}{AMSa}{"1C} +\DeclareMathSymbol\rightleftarrows{\mathrel}{AMSa}{"1D} +\DeclareMathSymbol\Lsh{\mathrel}{AMSa}{"1E} +\DeclareMathSymbol\Rsh{\mathrel}{AMSa}{"1F} +\DeclareMathSymbol\rightsquigarrow{\mathrel}{AMSa}{"20} +\DeclareMathSymbol\leftrightsquigarrow{\mathrel}{AMSa}{"21} +\DeclareMathSymbol\looparrowleft{\mathrel}{AMSa}{"22} +\DeclareMathSymbol\looparrowright{\mathrel}{AMSa}{"23} +\DeclareMathSymbol\circeq{\mathrel}{AMSa}{"24} +\DeclareMathSymbol\succsim{\mathrel}{AMSa}{"25} +\DeclareMathSymbol\gtrsim{\mathrel}{AMSa}{"26} +\DeclareMathSymbol\gtrapprox{\mathrel}{AMSa}{"27} +\DeclareMathSymbol\multimap{\mathrel}{AMSa}{"28} +\DeclareMathSymbol\therefore{\mathrel}{AMSa}{"29} +\DeclareMathSymbol\because{\mathrel}{AMSa}{"2A} +\DeclareMathSymbol\doteqdot{\mathrel}{AMSa}{"2B} +\DeclareMathSymbol\triangleq{\mathrel}{AMSa}{"2C} +\DeclareMathSymbol\precsim{\mathrel}{AMSa}{"2D} +\DeclareMathSymbol\lesssim{\mathrel}{AMSa}{"2E} +\DeclareMathSymbol\lessapprox{\mathrel}{AMSa}{"2F} +\DeclareMathSymbol\eqslantless{\mathrel}{AMSa}{"30} +\DeclareMathSymbol\eqslantgtr{\mathrel}{AMSa}{"31} +\DeclareMathSymbol\curlyeqprec{\mathrel}{AMSa}{"32} +\DeclareMathSymbol\curlyeqsucc{\mathrel}{AMSa}{"33} +\DeclareMathSymbol\preccurlyeq{\mathrel}{AMSa}{"34} +\DeclareMathSymbol\leqq{\mathrel}{AMSa}{"35} +\DeclareMathSymbol\leqslant{\mathrel}{AMSa}{"36} +\DeclareMathSymbol\lessgtr{\mathrel}{AMSa}{"37} +\DeclareMathSymbol\backprime{\mathord}{AMSa}{"38} +\DeclareMathSymbol\risingdotseq{\mathrel}{AMSa}{"3A} +\DeclareMathSymbol\fallingdotseq{\mathrel}{AMSa}{"3B} +\DeclareMathSymbol\succcurlyeq{\mathrel}{AMSa}{"3C} +\DeclareMathSymbol\geqq{\mathrel}{AMSa}{"3D} +\DeclareMathSymbol\geqslant{\mathrel}{AMSa}{"3E} +\DeclareMathSymbol\gtrless{\mathrel}{AMSa}{"3F} +\DeclareMathSymbol\sqsubset{\mathrel}{AMSa}{"40} +\DeclareMathSymbol\sqsupset{\mathrel}{AMSa}{"41} +\DeclareMathSymbol\vartriangleright{\mathrel}{AMSa}{"42} +\DeclareMathSymbol\vartriangleleft{\mathrel}{AMSa}{"43} +\DeclareMathSymbol\trianglerighteq{\mathrel}{AMSa}{"44} +\DeclareMathSymbol\trianglelefteq{\mathrel}{AMSa}{"45} +\DeclareMathSymbol\bigstar{\mathord}{AMSa}{"46} +\DeclareMathSymbol\between{\mathrel}{AMSa}{"47} +\DeclareMathSymbol\blacktriangledown{\mathord}{AMSa}{"48} +\DeclareMathSymbol\blacktriangleright{\mathrel}{AMSa}{"49} +\DeclareMathSymbol\blacktriangleleft{\mathrel}{AMSa}{"4A} +\DeclareMathSymbol\vartriangle{\mathord}{AMSa}{"4D} +\DeclareMathSymbol\blacktriangle{\mathord}{AMSa}{"4E} +\DeclareMathSymbol\triangledown{\mathord}{AMSa}{"4F} +\DeclareMathSymbol\eqcirc{\mathrel}{AMSa}{"50} +\DeclareMathSymbol\lesseqgtr{\mathrel}{AMSa}{"51} +\DeclareMathSymbol\gtreqless{\mathrel}{AMSa}{"52} +\DeclareMathSymbol\lesseqqgtr{\mathrel}{AMSa}{"53} +\DeclareMathSymbol\gtreqqless{\mathrel}{AMSa}{"54} +\DeclareMathSymbol\Rrightarrow{\mathrel}{AMSa}{"56} +\DeclareMathSymbol\Lleftarrow{\mathrel}{AMSa}{"57} +\DeclareMathSymbol\veebar{\mathbin}{AMSa}{"59} +\DeclareMathSymbol\barwedge{\mathbin}{AMSa}{"5A} +\DeclareMathSymbol\doublebarwedge{\mathbin}{AMSa}{"5B} +\DeclareMathSymbol\angle{\mathord}{AMSa}{"5C} +\DeclareMathSymbol\measuredangle{\mathord}{AMSa}{"5D} +\DeclareMathSymbol\sphericalangle{\mathord}{AMSa}{"5E} +\DeclareMathSymbol\varpropto{\mathrel}{AMSa}{"5F} +\DeclareMathSymbol\smallsmile{\mathrel}{AMSa}{"60} +\DeclareMathSymbol\smallfrown{\mathrel}{AMSa}{"61} +\DeclareMathSymbol\Subset{\mathrel}{AMSa}{"62} +\DeclareMathSymbol\Supset{\mathrel}{AMSa}{"63} +\DeclareMathSymbol\Cup{\mathbin}{AMSa}{"64} +\DeclareMathSymbol\Cap{\mathbin}{AMSa}{"65} +\DeclareMathSymbol\curlywedge{\mathbin}{AMSa}{"66} +\DeclareMathSymbol\curlyvee{\mathbin}{AMSa}{"67} +\DeclareMathSymbol\leftthreetimes{\mathbin}{AMSa}{"68} +\DeclareMathSymbol\rightthreetimes{\mathbin}{AMSa}{"69} +\DeclareMathSymbol\subseteqq{\mathrel}{AMSa}{"6A} +\DeclareMathSymbol\supseteqq{\mathrel}{AMSa}{"6B} +\DeclareMathSymbol\bumpeq{\mathrel}{AMSa}{"6C} +\DeclareMathSymbol\Bumpeq{\mathrel}{AMSa}{"6D} +\DeclareMathSymbol\lll{\mathrel}{AMSa}{"6E} +\DeclareMathSymbol\ggg{\mathrel}{AMSa}{"6F} +\DeclareMathDelimiter\ulcorner{4}{AMSa}{"70}{AMSa}{"70} +\DeclareMathDelimiter\urcorner{5}{AMSa}{"71}{AMSa}{"71} +\DeclareMathDelimiter\llcorner{4}{AMSa}{"78}{AMSa}{"78} +\DeclareMathDelimiter\lrcorner{5}{AMSa}{"79}{AMSa}{"79} +\xdef\yen {\noexpand\mathhexbox\hexnumber@\symAMSa 55 } +\xdef\checkmark{\noexpand\mathhexbox\hexnumber@\symAMSa 58 } +\xdef\circledR {\noexpand\mathhexbox\hexnumber@\symAMSa 72 } +\xdef\maltese {\noexpand\mathhexbox\hexnumber@\symAMSa 7A } +\DeclareMathSymbol\circledS{\mathord}{AMSa}{"73} +\DeclareMathSymbol\pitchfork{\mathrel}{AMSa}{"74} +\DeclareMathSymbol\dotplus{\mathbin}{AMSa}{"75} +\DeclareMathSymbol\backsim{\mathrel}{AMSa}{"76} +\DeclareMathSymbol\backsimeq{\mathrel}{AMSa}{"77} +\DeclareMathSymbol\complement{\mathord}{AMSa}{"7B} +\DeclareMathSymbol\intercal{\mathbin}{AMSa}{"7C} +\DeclareMathSymbol\circledcirc{\mathbin}{AMSa}{"7D} +\DeclareMathSymbol\circledast{\mathbin}{AMSa}{"7E} +\DeclareMathSymbol\circleddash{\mathbin}{AMSa}{"7F} +% \end{macrocode} +% +%AMSb font: +% +% \begin{macrocode} +\DeclareMathSymbol\lvertneqq{\mathrel}{AMSb}{"00} +\DeclareMathSymbol\gvertneqq{\mathrel}{AMSb}{"01} +\DeclareMathSymbol\nleq{\mathrel}{AMSb}{"02} +\DeclareMathSymbol\ngeq{\mathrel}{AMSb}{"03} +\DeclareMathSymbol\nless{\mathrel}{AMSb}{"04} +\DeclareMathSymbol\ngtr{\mathrel}{AMSb}{"05} +\DeclareMathSymbol\nprec{\mathrel}{AMSb}{"06} +\DeclareMathSymbol\nsucc{\mathrel}{AMSb}{"07} +\DeclareMathSymbol\lneqq{\mathrel}{AMSb}{"08} +\DeclareMathSymbol\gneqq{\mathrel}{AMSb}{"09} +\DeclareMathSymbol\nleqslant{\mathrel}{AMSb}{"0A} +\DeclareMathSymbol\ngeqslant{\mathrel}{AMSb}{"0B} +\DeclareMathSymbol\lneq{\mathrel}{AMSb}{"0C} +\DeclareMathSymbol\gneq{\mathrel}{AMSb}{"0D} +\DeclareMathSymbol\npreceq{\mathrel}{AMSb}{"0E} +\DeclareMathSymbol\nsucceq{\mathrel}{AMSb}{"0F} +\DeclareMathSymbol\precnsim{\mathrel}{AMSb}{"10} +\DeclareMathSymbol\succnsim{\mathrel}{AMSb}{"11} +\DeclareMathSymbol\lnsim{\mathrel}{AMSb}{"12} +\DeclareMathSymbol\gnsim{\mathrel}{AMSb}{"13} +\DeclareMathSymbol\nleqq{\mathrel}{AMSb}{"14} +\DeclareMathSymbol\ngeqq{\mathrel}{AMSb}{"15} +\DeclareMathSymbol\precneqq{\mathrel}{AMSb}{"16} +\DeclareMathSymbol\succneqq{\mathrel}{AMSb}{"17} +\DeclareMathSymbol\precnapprox{\mathrel}{AMSb}{"18} +\DeclareMathSymbol\succnapprox{\mathrel}{AMSb}{"19} +\DeclareMathSymbol\lnapprox{\mathrel}{AMSb}{"1A} +\DeclareMathSymbol\gnapprox{\mathrel}{AMSb}{"1B} +\DeclareMathSymbol\nsim{\mathrel}{AMSb}{"1C} +\DeclareMathSymbol\ncong{\mathrel}{AMSb}{"1D} +%\DeclareMathSymbol\varsubsetneq{\mathrel}{AMSb}{"20} +%\DeclareMathSymbol\varsupsetneq{\mathrel}{AMSb}{"21} +\DeclareMathSymbol\nsubseteqq{\mathrel}{AMSb}{"22} +\DeclareMathSymbol\nsupseteqq{\mathrel}{AMSb}{"23} +\DeclareMathSymbol\subsetneqq{\mathrel}{AMSb}{"24} +\DeclareMathSymbol\supsetneqq{\mathrel}{AMSb}{"25} +%\DeclareMathSymbol\varsubsetneqq{\mathrel}{AMSb}{"26} +%\DeclareMathSymbol\varsupsetneqq{\mathrel}{AMSb}{"27} +\DeclareMathSymbol\subsetneq{\mathrel}{AMSb}{"28} +\DeclareMathSymbol\supsetneq{\mathrel}{AMSb}{"29} +\DeclareMathSymbol\nsubseteq{\mathrel}{AMSb}{"2A} +\DeclareMathSymbol\nsupseteq{\mathrel}{AMSb}{"2B} +\DeclareMathSymbol\nparallel{\mathrel}{AMSb}{"2C} +\DeclareMathSymbol\nmid{\mathrel}{AMSb}{"2D} +\DeclareMathSymbol\nshortmid{\mathrel}{AMSb}{"2E} +\DeclareMathSymbol\nshortparallel{\mathrel}{AMSb}{"2F} +\DeclareMathSymbol\nvdash{\mathrel}{AMSb}{"30} +\DeclareMathSymbol\nVdash{\mathrel}{AMSb}{"31} +\DeclareMathSymbol\nvDash{\mathrel}{AMSb}{"32} +\DeclareMathSymbol\nVDash{\mathrel}{AMSb}{"33} +\DeclareMathSymbol\ntrianglerighteq{\mathrel}{AMSb}{"34} +\DeclareMathSymbol\ntrianglelefteq{\mathrel}{AMSb}{"35} +\DeclareMathSymbol\ntriangleleft{\mathrel}{AMSb}{"36} +\DeclareMathSymbol\ntriangleright{\mathrel}{AMSb}{"37} +\DeclareMathSymbol\nleftarrow{\mathrel}{AMSb}{"38} +\DeclareMathSymbol\nrightarrow{\mathrel}{AMSb}{"39} +\DeclareMathSymbol\nLeftarrow{\mathrel}{AMSb}{"3A} +\DeclareMathSymbol\nRightarrow{\mathrel}{AMSb}{"3B} +\DeclareMathSymbol\nLeftrightarrow{\mathrel}{AMSb}{"3C} +\DeclareMathSymbol\nleftrightarrow{\mathrel}{AMSb}{"3D} +\DeclareMathSymbol\divideontimes{\mathbin}{AMSb}{"3E} +\DeclareMathSymbol\varnothing{\mathord}{AMSb}{"3F} +\DeclareMathSymbol\mho{\mathord}{AMSb}{"66} +\DeclareMathSymbol\eth{\mathord}{AMSb}{"67} +\DeclareMathSymbol\eqsim{\mathrel}{AMSb}{"68} +\DeclareMathSymbol\beth{\mathord}{AMSb}{"69} +\DeclareMathSymbol\gimel{\mathord}{AMSb}{"6A} +\DeclareMathSymbol\daleth{\mathord}{AMSb}{"6B} +\DeclareMathSymbol\lessdot{\mathrel}{AMSb}{"6C} +\DeclareMathSymbol\gtrdot{\mathrel}{AMSb}{"6D} +\DeclareMathSymbol\ltimes{\mathbin}{AMSb}{"6E} +\DeclareMathSymbol\rtimes{\mathbin}{AMSb}{"6F} +\DeclareMathSymbol\shortmid{\mathrel}{AMSb}{"70} +\DeclareMathSymbol\shortparallel{\mathrel}{AMSb}{"71} +\DeclareMathSymbol\smallsetminus{\mathbin}{AMSb}{"72} +\DeclareMathSymbol\thicksim{\mathrel}{AMSb}{"73} +\DeclareMathSymbol\thickapprox{\mathrel}{AMSb}{"74} +\DeclareMathSymbol\approxeq{\mathrel}{AMSb}{"75} +\DeclareMathSymbol\succapprox{\mathrel}{AMSb}{"76} +\DeclareMathSymbol\precapprox{\mathrel}{AMSb}{"77} +\DeclareMathSymbol\curvearrowleft{\mathrel}{AMSb}{"78} +\DeclareMathSymbol\curvearrowright{\mathrel}{AMSb}{"79} +\DeclareMathSymbol\digamma{\mathord}{AMSb}{"7A} +\DeclareMathSymbol\varkappa{\mathord}{AMSb}{"7B} +\DeclareMathSymbol\hslash{\mathord}{AMSb}{"7D} +\DeclareMathSymbol\hbar{\mathord}{AMSb}{"7E} +\DeclareMathSymbol\backepsilon{\mathrel}{AMSb}{"7F} +} +\def\interleave{{\parallel\!\!\vert}} +\def\shortinterleave{\z@rel{\mathord\shortmid\mathord\shortparallel}} +\def\napprox{\not\approx} +\let\restriction\upharpoonright +\let\Doteq\doteqdot +\let\doublecup\Cup +\let\llless\lll +\let\gggtr\ggg +\let\doublecap\Cap +% \end{macrocode} +% +% Numbers +% +% \begin{macrocode} +\def \nat {{\mathbb N}} +\def \integer {{\mathbb Z}} +\def \natone {{\mathbb N}_1} +\def \real {{\mathbb R}} +\def \bool {{\mathbb B}} +\let \divides \div +\def \div {\z@bin{\mathrm{div}}} +\def \mod {\z@bin{\mathrm{mod}}} +\def \succ {\word{succ}} +\def \expon {^} +% \end{macrocode} +% aliases +% \begin{macrocode} +\let \num \integer +\let \nplus \natone +% \end{macrocode} +% +% Logic +% +% \begin{macrocode} +\def \lnot {\neg\;} +\def \land {\z@rel{\wedge}} +\def \lor {\z@rel{\vee}} +\let \imp \Rightarrow +\let\iff \Leftrightarrow +\def \all {\z@op{\xforall}} +\def \exi {\z@op{\xexists}} +\def \exione {\exists_1} +\@ifpackageloaded{lucbr}{% +\DeclareMathSymbol{\nexi}{0}{arrows}{"20} +}{% +\DeclareMathSymbol{\nexi}{\mathord}{AMSb}{"40} +} +\def \dot {\z@rel{\bullet}} +\def \true {\keyword{true}} +\def \false {\keyword{false}} +\let \cond \rightarrow +% \end{macrocode} +% aliases +% \begin{macrocode} +\let \spot \dot +\mathcode`\@="8000% make @ active in mathmode +{\catcode`\@=\active \gdef@{\dot}} +\let \implies \imp +\let \forall \all +\let \exists \exi +\let \nexists \nexi +% \end{macrocode} +% +% SETS +% +% \begin{macrocode} +\let \emptyset \varnothing +\def \varemptyset {\{\,\}} +\def \pset {\z@op{\mathbb P}} +\def \psetone {\pset_1} +\def \fset {\z@op{\mathbb F}} +\def \fsetone {\fset_1} +\def \sset {\z@op{\mathbb S}} +\let \mem \in +\def \nem {\not\mem} +\def \uni {\z@bin\cup} +\def \int {\z@bin\cap} +\let \prod \times +\def \min {\word{min}} +\def \max {\word{max}} +\def \duni {\z@Bigop{\lower0.25ex\hbox{$\uni$}}} +\def \dint {\z@Bigop{\lower0.25ex\hbox{$\int$}}} +\def \upto {\z@bin{\ldotp\ldotp}} +\let \psubs \subset +\let \subs \subseteq +\let \psups \supset +\let \sups \supseteq +\def \diff {\z@bin{\backslash}} +% \end{macrocode} +% aliases +% \begin{macrocode} +\let \cross \prod +\let \notin \nem +\let \nmem \nem +\let \union \uni +\let \inter \int +\let \power \pset +\let \finset \fset +\let \dunion \duni +\let \dinter \dint +% \end{macrocode} +% +% RELATIONS \& FUNCTIONS +% +% \begin{macrocode} +\def \lambda {\z@op{\xlambda}} +\def \mu {\z@op{\xmu}} +\def \dom {\keyword{dom}} +\def \ran {\keyword{ran}} +\def \id {\keyword{id}} +\@ifpackageloaded{lucbr}{% +\DeclareMathSymbol{\dres}{\mathbin}{letters}{"2F} +\DeclareMathSymbol{\rres}{\mathbin}{letters}{"2E} +}{% +\DeclareMathSymbol{\dres}{\mathbin}{AMSa}{"43} +\DeclareMathSymbol{\rres}{\mathbin}{AMSa}{"42} +} +\def \dsub {\mathbin{\rlap{\raise.05ex\hbox{$-$}}{\dres}}} +\def \rsub {\mathbin{\rlap{\raise.05ex\hbox{$-$}}{\rres}}} +\let \fovr \oplus +\let \cmp \circ +\def \fcmp {\mathbin{\raise 0.6ex\hbox{\oalign{\hfil$\scriptscriptstyle + \mathrm{o}$\hfil\cr\hfil$\scriptscriptstyle\mathrm{9}$\hfil}}}} +\def \inv {^\sim} +\def \limg {(\!|} +\def \rimg {|\!)} +\let \map \mapsto +\let \rel \leftrightarrow +\let \tfun \rightarrow +\let \tinj \rightarrowtail +\def \tsur {\mathrel{\ooalign{$\tfun$\hfil\cr$\mkern4mu\tfun$}}} +\def \pfun {\p\tfun} +\def \pinj {\p\tinj} +\def \psur {\p\tsur} +\def \ffun {\f\tfun} +\def \finj {\f\tinj} +\def \bij {\mathrel{\ooalign{$\tinj$\hfil\cr$\mkern5mu\tfun$}}} +\def \tcl {^+} +\def \rtcl {^*} +\def \iter {^} +% \end{macrocode} +% aliases +% \begin{macrocode} +\let \comp \fcmp +\let \ndres \dsub +\let \nrres \rsub +\let \fun \tfun +\let \inj \tinj +\let \surj \tsur +\let \psurj \psur +\let \llless \lll +\let \gggtr \ggg +\def \interleave {{\parallel\!\!\vert}} +\def \shortinterleave {\z@rel{\mathord\shortmid\mathord\shortparallel}} +\let \restriction \upharpoonright +\def \napprox {\not\approx} +% \end{macrocode} +% +% SEQUENCES +% \begin{macrocode} +\def \seq {\keyword{seq}} +\def \iseq {\keyword{iseq}} +\def \seqone {\seq_1} +\def \emptyseq {\lseq\,\rseq} +\let \lseq \langle +\let \rseq \rangle +\def \head {\word{head}} +\def \tail {\word{tail}} +\def \front {\word{front}} +\def \last {\word{last}} +\def \rev {\word{rev}} +\def \squash {\word{squash}} +\def \next {\keyword{next}} +\def \inseq {\keyword{in}} +\@ifpackageloaded{lucbr}{% +\DeclareMathSymbol{\sres}{2}{arrows}{"75} +\DeclareMathSymbol{\ires}{2}{arrows}{"76} +\DeclareMathSymbol{\@@cat}{\mathbin}{operators}{"5F} +}{% +\DeclareMathSymbol{\@@cat}{\mathbin}{AMSa}{"61} +\DeclareMathSymbol{\sres}{\mathbin}{AMSa}{"16} +\DeclareMathSymbol{\ires}{\mathbin}{AMSa}{"18} +} +\def \cat {\mathbin{\raise 0.8ex\hbox{$\mathchar\@@cat$}}} +\def \ssub {\z@bin{\rlap{$-$}{\sres}}} +\def \isub {\z@bin{\rlap{$-$}{\ires}}} +\def \dcat {\z@op{\cat/}} +\def \dovr {\z@op{\fovr/}} +\def \dcmp {\z@op{\fcmp/}} +\let \prefix \subseteq +\def \suffix {\keyword{suffix}} +\def \seqi {\keyword{seq_\infty}} +\def \partitions {\keyword{partitions}} +\def \partition {\keyword{partitions}} +\def \disjoint {\keyword{disjoint}} +\def \subseq {\keyword{subseq}} +% \end{macrocode} +% aliases +% \begin{macrocode} +\let \filter \sres +% \end{macrocode} +% +% Schemas: +% +% \begin{macrocode} +\def \lsch {\z@bigop{[}} +\def \rsch {\z@bigop{]}} +\def \dparallel {\z@bigop{\parallel}\limits} +\def \zand {\z@bigbin\land} +\def \zor {\z@bigbin\lor} +\def \zcmp {\z@bigbin\fcmp} +\def \zexi {\z@bigop\exists} +\def \zall {\z@bigop\forall} +\def \znot {\z@bigop\neg} +\def \zbar {\z@bigbin\cbar} +\def \zfor {/} +\def \zhide {\z@bigbin\backslash} +\def \zimp {\z@bigrel\imp} +\def \zeq {\z@bigrel\iff} +\def \zovr {\z@bigrel\oplus} +\def \zpipe {\z@bigbin{\mathord>\!\!\mathord>}} +\def \pre {\keyword{pre}} +\def \pred {\keyword{pred}} +\def \post {\keyword{post}} +\def \zproject {\z@bigbin\sres} +\def\rename{\@ifnextchar*{\z@rename}{\z@@rename}} +\def\z@rename*[#1/#2]{\left[#1 \over #2\right]} +\def\z@@rename[#1/#2]{\left[#1 \zfor #2\right]} +% \end{macrocode} +% aliases +% \begin{macrocode} +\let \project \zproject +\let \import \sres +\let \semi \zcmp +\let \hide \zhide +% \end{macrocode} +% +% BAGS +% +% \begin{macrocode} +\let\buni\uplus +\def \emptybag {\lbag\:\rbag} +\def \lbag {[\![} +\def \rbag {]\!]} +\def \bag {\keyword{bag}} +\def \items {\word{items}} +\let \inbag \inseq +\def \bagcount {\word{count}} +% \end{macrocode} +% +% Definitions \& declarations +% +% \begin{macrocode} +\def \ddef {\z@rel{\;::=\;}} +\def \bbar {\z@bigrel{|}} +\let \cbar \mid +\def \lang {\langle\!\langle} +\def \rang {\rangle\!\rangle} +\def \sdef {\z@rel{\widehat=}} +\def \defs {\z@smallrel{==}} +\def \varsdef {\z@rel\triangleq} +% \end{macrocode} +% aliases +% \begin{macrocode} +\let \sdefs \sdef +\mathcode`\|=\mid +\let \ldata \lang +\let \rdata \rang +% \end{macrocode} +% +% MISCELLANEOUS +% +% \begin{macrocode} +\def \lblot {\langle\!|} +\def \rblot {|\!\rangle} +\def \IMP {\boldword{Import}} +\let \env \Rrightarrow +\def \zlet {\boldword{let}} +\def \zin {\boldword{in}} +\def \zwhere {\boldword{where}} +% \end{macrocode} +% +% QZED SUPPORT +% +% \begin{macrocode} +\def\HOLE{\z@op{\hbox{$\lll\star\star\star\ggg$}}} +\def\landd{} % to support qzed editor +\def\semid{} % to support qzed editor +\def\qzed{\ifz@inclass\else\zed\fi} +\def\endqzed{\ifz@inclass\else\endzed\fi} +% \end{macrocode} +% +% CLASSES +% +% \begin{macrocode} +\def\qua{\mbox{::}} +\def\redef{\mbox{\textbf{~redef}}} +\def\Init{I\!{\scriptstyle{NIT}}} +\def\Exit{E\!{\scriptstyle{XIT}}} +\def\Internal{I\!{\scriptstyle{NTERNAL}}} +\def\Aux{A\!{\scriptstyle{UX}}} +\def\intern{\mbox{\textsf{i}}} +% \end{macrocode} +% +% PROOFS +% +% \begin{macrocode} +\def\thrm{\z@rel\vdash} +\def\qed{\zsmall\Box} +\let\Qed\Box +\let\QED\square +\def\BLACKQED{\zsmall\blacksquare} +\let\ETH\qed +\def\TH{\boldword{Theorem}} +\def\LE{\boldword{Lemma}} +\def\PR{\boldword{Proof}} +\def\refines{\z@rel\sqsupseteq} +\def\defines{\z@rel\sqsubseteq} +\def\weakrefine{\z@rel{\raise0.2ex\rlap{\hbox{$\sqsupset$}}\lower1ex\hbox{$\sim$}}} +\def\weakdefine{\z@rel{\raise0.2ex\rlap{\hbox{$\sqsubset$}}\lower1ex\hbox{$\sim$}}} +% \end{macrocode} +% aliases +% \begin{macrocode} +\let\shows\thrm +% \end{macrocode} +% +% OBJECT THEORY +% +% \begin{macrocode} +\def\childof{\z@rel\xsucc} +\def\parentof{\z@rel\xprec} +\let\weaksubclass\succsim +\let\weaksupclass\precsim +\def\hasa{\z@rel{\mathord\xsucc\!\!\!\mathord\xsucc}} +\def\instancein{\z@rel{\mathord\xprec\!\!\!\mathord\xprec}} +\def\subtype{\z@rel\sqsubset} +\def\subtypeeq{\z@rel\sqsubseteq} +\def\suptype{\z@rel\sqsupset} +\def\suptypeeq{\z@rel\sqsupseteq} +% \end{macrocode} +% aliases +% \begin{macrocode} +\let\inherits\childof +\let\subclass\childof +\let\isa\childof +\let\supclass\parentof +\let\instantiates\hasa +\let\islikea\weaksubclass +\def\poly{\mathord\downarrow} +\def\widen#1{\z@op{{\overline{#1}}}} +% \end{macrocode} +% +% TEMPORAL LOGIC +% +% \begin{macrocode} +\def\atnext{\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\zSmall\bigcirc$}\kern0.01em\zSmall\bigcirc} +\def\atlast{\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\kern0.01em\mathord-$}\zSmall\bigcirc} +\def\always{\lower0.37ex\hbox{$\zbig\Box$}} +\def\uptilnow{\rlap{$\kern0.02em\mathord-$}\lower0.37ex\hbox{$\zbig\Box$}} +\def\eventually{\lower0.37ex\hbox{$\zbig\Diamond$}} +\def\previously{\rlap{$\kern0.04em\mathord-$}\lower0.37ex\hbox{$\zbig\Diamond$}} +% \end{macrocode} +% aliases +% \begin{macrocode} +\let\henceforth\always +% \end{macrocode} +% +% ORDERS +% +% \begin{macrocode} +\def \mono {\keyword{monotonic}} +\def \porder {\keyword{partial\_order}} +\def \torder {\keyword{total\_order}} +\newbox\z@combox\newdimen\z@wdcalc +\def\comment{\@ifnextchar*{\z@leftcomment}{\z@comment}} +\def\z@comment#1{$\z@stopfield\z@addfield\z@startfield$% +\global\setbox\z@combox\hbox{\quad[{\sf #1}]}\z@wdcalc=\wd\z@combox% +\advance\z@wdcalc by \wd\z@curline\advance\z@wdcalc by \z@curindent% +\advance\z@wdcalc by \zedleftsep\advance\z@wdcalc by \zedlinethickness% +\advance\z@wdcalc by 2\zedindent\ifdim\z@wdcalc>\displaywidth\\% +\fi&\box\z@combox\ignorespaces} +\def\z@leftcomment*#1{\hbox{[{\sf #1}]}} +% \end{macrocode} +% +%\section{Object-Z Notations} +% +% KEYWORDS AND KEYSYMBOLS +% +% \begin{macrocode} +\def \oid {{\bbold O}} +\def \self {\word{self}} +\def \contained {\word{contained}} +\let \classuni \uni +\def \visibility {\zproject} +\def \invisibility {{\project\hspace{-0.63 em}\cross}} +% \end{macrocode} +% +% CONTAINMENT AND CONTROL ADORNMENTS +% +% \begin{macrocode} +\def \cid {{\bigcirc\mbox{\scriptsize{\hspace{-0.78em}}\mbox{\tiny{C}}}}} +\def \sid {{\bigcirc\mbox{\scriptsize{\hspace{-0.74em}}\mbox{\tiny{S}}}}} +\def \eid {{\bigcirc\mbox{\scriptsize{\hspace{-0.74em}}\mbox{\tiny{E}}}}} +% \end{macrocode} +% +% BINARY COMPOSITION OPERATORS +% +% \begin{macrocode} +\def \pll {~\parallel~} +\def \plo {~\parallel_{!}~} +\def \sqc {~\semi~} +\def \cnj {~\zand~} +\def \gch {~[\mbox{\hspace{-0.06em}}]~} +\def \enh {~\dot~} +% \end{macrocode} +% +% DISTRIBUTED COMPOSITION OPERATORS +% +% \begin{macrocode} +% Redefined because of \zbig problem +% \def \dsqc {\mbox{{\Large $\zcmp~$}}} +\def \dsqc {\mbox{{\Large $\fcmp~$}}} +\def \dgch {\mbox{{\Large $[\mbox{\hspace{-0.06em}}]$}}} +% Redefined because of \zbig problem +% \def \dcnj {\mbox{{\Large $\zand$}}} +\def \dcnj {\mbox{{\Large $\land$}}} +\def \dpll {\mbox{{\Large $\parallel$}}} +\def \dplo {\mbox{{\Large $\parallel_{!}$}}} +% \end{macrocode} +% +%\section{Z environments} +% +%\subsection{Margin stack} +% +% Define a stack of dimensions (50 elements) +% This can probably be made smaller when qzed filters its \TeX\ output better +% \begin{macrocode} +\newcount\z@stackmin +\newcount\z@stackmax +\newcount\z@stacktop +\newdimen\@gtempa \z@stackmin=\allocationnumber +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa +\z@stackmax=\allocationnumber +\dimen\z@stackmin=0pt +% \end{macrocode} +% Define a box to contain the current line +% \& a variable to contain it's indentation +% \begin{macrocode} +\newbox\z@curline +\newdimen\z@curindent +\dimen\z@curindent=0pt +% \end{macrocode} +% Space between operands of a function application +% \begin{macrocode} +\def\z@space{{}\;{}} +% \end{macrocode} +% Define a box to contain the current field +% \begin{macrocode} +\newbox\z@curfield +% \end{macrocode} +% Define a mini-tabbing environment for use inside `zed' +% \begin{macrocode} +\def\z@startline{\setbox\z@curline\hbox{}% + \global\z@curindent\dimen\z@stacktop + \z@startfield\ignorespaces} +\def\z@stopline{\z@stopfield + \z@addfield + \hbox{\hskip\z@curindent \box\z@curline}} + +\def\z@startfield{\global\setbox\z@curfield\hbox\bgroup} +\def\z@stopfield{\egroup} +\def\z@addfield{\global\setbox\z@curline\hbox{\unhbox + \z@curline\unhbox\z@curfield}} + +\def\z@pushmargin{\hbox{\kern0pt}$% + \z@stopfield + \z@addfield + \ifnum \z@stacktop < \z@stackmax + \global\advance\z@stacktop \@ne + \else + \@latexerr{Z margin stack overflow (too many \string\M's)} + \@ehd + \fi + \global\dimen\z@stacktop\z@curindent + \global\advance\dimen\z@stacktop \wd\z@curline + \z@startfield\ignorespaces + $\relax} +\def\z@popmargin{\ifnum \z@stacktop > \z@stackmin + \global\advance\z@stacktop \m@ne \ignorespaces + \else + \@latexerr{Z Margin stack underflow (too many \string\O's)} + \@ehd + \fi} +\def\M{\z@pushmargin} \def\O{\z@popmargin} \def\S{\z@space} +\z@stacktop\z@stackmin +% \end{macrocode} +% +%\subsection{Utility macros for Z environments} +% +% Here are environments for the various sorts of displays which occur in +% Z documents. All displays are set flush left, indented by |\zedindent|, +% by default |\leftmargini|. Schemas, etc, are made just wide enough to +% give equal margins left and right. +% +% Some environments (schema, etc.) must only be split at |\zbreak|, +% and others (e.g. argue) may be split arbitrarily. All generate +% alignment displays, and penalties are used to control page breaks. +% +%\subsubsection{Format and control macros} +% +% \begin{macrocode} +\newdimen\zedindent \zedindent=\leftmargini +\newdimen\zedleftsep \zedleftsep=1em +\newdimen\zedtab \zedtab=2em +\newdimen\zedbar \zedbar=8em +\newdimen\zedlinethickness \zedlinethickness=0.4pt +\newdimen\zedcornerheight \zedcornerheight=0pt +\newcount\z@cols +\newif\ifz@firstline \z@firstlinefalse +\newif\ifz@inclass \z@inclassfalse +\newif\ifz@inenv \z@inenvfalse +\newif\ifz@leftmargin \z@leftmargintrue +\newif\ifz@incols \z@incolsfalse +\newif\ifleftnames \leftnamesfalse +\def\leftschemas{\leftnamestrue} +\newif\ifz@inbox \z@inboxfalse +\newskip\zedbaselineskip \zedbaselineskip\baselineskip +\newbox\zstrutbox \setbox\zstrutbox=\copy\strutbox +\def\zstrut{\relax\ifmmode\copy\zstrutbox\else\unhcopy\zstrutbox\fi} +\def\zedbaselinestretch{1} +\def\baselinestretch{1} +% \end{macrocode} +% +% Penalties +% +% \begin{macrocode} +\newcount\interzedlinepenalty \interzedlinepenalty=10000 %never break +\newcount\preboxpenalty \preboxpenalty=0 %break easily +\newcount\forcepagepenalty \forcepagepenalty=-10000 %always break +\interdisplaylinepenalty=100 %break sometimes +% \end{macrocode} +% +% Macros for changing the size of schema text +% +% \begin{macrocode} +\def\zedsize#1{\def\z@size{#1}} +\def\z@size{} +\newskip\z@adskip\newskip\z@bdskip\newskip\z@adsskip\newskip\z@bdsskip +\def\z@changesize{% +\z@adskip\abovedisplayskip\z@bdskip\belowdisplayskip% save skips +\z@adsskip\abovedisplayshortskip\z@bdsskip\belowdisplayshortskip +\z@size % change size +\abovedisplayskip\z@adskip\belowdisplayskip\z@bdskip% restore skips +\abovedisplayshortskip\z@adsskip\belowdisplayshortskip\z@bdsskip} +% +\def\z@zeroskips{\abovedisplayskip\z@\belowdisplayskip\z@ + \abovedisplayshortskip\z@\belowdisplayshortskip\z@} +% +% Make zedbaselinestretch have an automatic effect +% adapted from lfonts.tex +% +\def\@setfontsize#1#2#3{\@nomath#1% + \ifx\protect\@typeset@protect + \let\@currsize#1% + \fi + \fontsize{#2}{#3}\selectfont + \setlength{\zedbaselineskip}{\baselineskip/\real{\baselinestretch}}% + \zedbaselineskip\zedbaselinestretch\zedbaselineskip + \setbox\zstrutbox\hbox{\vrule height.7\zedbaselineskip + depth.3\zedbaselineskip width\z@}} +% \end{macrocode} +% +%\subsection{Macros for margins} +% +% |\z@narrow|, |\z@wide| --- make the margins narrower, wider +% +% \begin{macrocode} +\def\z@narrow{\advance\linewidth by -\zedindent} +\def\z@wide{\advance\linewidth by \zedindent} +% \end{macrocode} +% +%\subsection{Macros for drawing boxes} +% +% |\z@hrulefill| --- line with correct thickness +% +% \begin{macrocode} +\def\z@hrulefill{\leaders\hrule height\zedlinethickness\hfill} +% \end{macrocode} +% +% |\z@topline| draws the top horizontal line of boxed environments +% |\z@dbltopline| draws a double ruled top line +% |\z@botline| draws the bottom horizontal line of boxed environments +% |\zedline[comment]| draws a long horizontal line ending in comment +% |\where| draws a short horizontal line +% +% \begin{macrocode} +\def\z@topline#1{\omit\@ifnextchar[{\z@@topline{#1}}{\z@@topline{#1}[]}} +\def\z@@topline#1[#2]{\hbox to\linewidth{\zstrut\ifleftnames\else + \vrule height\zedlinethickness width\zedlinethickness + \hbox to\zedleftsep{\z@hrulefill}\fi#1\z@hrulefill + \smash{\vrule height\zedlinethickness width\zedlinethickness + depth\zedcornerheight}\hbox{\sf #2}}\cr} +\def\z@dbltopline#1{\omit\@ifnextchar[{\z@@dbltopline{#1}}{\z@@dbltopline{#1}[]}} +\def\z@@dbltopline#1[#2]{\z@@topline{#1}[#2]% +\noalign{\kern-\baselineskip + \kern-\zedlinethickness + \kern-\doublerulesep \nobreak}% +\omit\z@@topline{\hphantom{#1}}[\hphantom{#2}]% +\noalign{\kern\doublerulesep + \kern\zedlinethickness \nobreak}} +\def\z@botline{\also\omit\hbox to\linewidth{\z@hrulefill +\smash{\vrule height\zedcornerheight width\zedlinethickness + depth 0pt}}\cr} +\def\z@@botline[#1]{\hbox to\linewidth{\vrule\z@hrulefill\hbox{\sf\smash{#1}}}\also} +\def\zedline{\also\omit\@ifnextchar[{\z@@botline}{\z@@botline[]}} +\def\where{\also \omit \hbox to\zedbar{\z@hrulefill}\cr\also} +\let \ST \where +% \end{macrocode} +% +% |\z@left| is placed at the left of each z line: +% in non-box environments it will do nothing. +% in boxed environments it will do a vertical line with the same +% height as the maximum height of the line. +% +% \begin{macrocode} +\def\z@left{\ifz@inbox\vrule width\zedlinethickness\hskip\zedleftsep\fi} +% \end{macrocode} +% +% \subsection{Macros for setting up Z environments} +% +% \begin{macrocode} +\def\z@env{\global\z@firstlinetrue\z@changesize + $$ + \z@inenvtrue + \baselineskip\zedbaselineskip + \parskip=0pt\lineskip=0pt\z@narrow + \advance\displayindent by \zedindent + \def\\{\crcr}% Must have \def and not \let for nested alignments. + \everycr={\noalign{\ifz@firstline \global\z@firstlinefalse + \else \penalty\interzedlinepenalty \fi}} + \tabskip=0pt} +\def\endz@env{$$ + \global\@ignoretrue +} +% \end{macrocode} +% +% Z lines are formated in two (overlapping) columns; +% the first flush left having the same width as the environment, +% and, the second flush right ending at the right end of the environment. +% +% \begin{macrocode} +\def\z@format{\halign to\linewidth\bgroup% + \zstrut\z@left\z@startline\ignorespaces$\@lign##$\z@stopline\hfil% + \tabskip=0pt plus1fil% + &\hbox to 0pt{\hss\@lign##}\tabskip=0pt\cr} +\def\z@boxenv{\z@narrow\let\also=\als@ \let\Also=\Als@ \let\ALSO=\ALS@ + \z@inboxtrue \predisplaypenalty=\preboxpenalty \z@env\z@format} +\def\z@outnonbox{\z@outclasscheck\z@leavevmode\z@env} +\def\z@inoutbox{\z@leavevmode\z@makeouter\z@inclassfalse\z@boxenv} +% \end{macrocode} +% +%\subsection{Spacing commands} +% +% no vertical glue between abutted lines +% +% \begin{macrocode} +\def\@but{\noalign{\nointerlineskip}} +% \end{macrocode} +% +% no |\par| extra vertical spacing after Z environments +% +%|\def\z@nopar{\ifz@inclass\else\vskip-\parskip\fi}| +%|\def\z@nopar{\global\parskip0pt\global\everypar{\parskip30mm\everypar{}}}| +% \begin{macrocode} +\def\z@nopar{\global\@endpetrue} +% \end{macrocode} +% +% |\z@leavevmode| -- Enter horizontal mode, taking account of possible +% interaction with lists and section heads: +%\begin{enumerate} +% \item After a |\item|, use |\indent| to get the label (this +% fails to run in even short labels). +% \item After a run-in heading, use |\indent|. +% \item After an ordinary heading, throw away the |\everypar| +% tokens, reset |\@nobreak|, and use |\noindent| with |\parskip| +% zero. +% \item Otherwise, use |\noindent| with |\parskip| zero +%\end{enumerate} +% Use when entering displayed environments to get correct spacing +% +% \begin{macrocode} +\def\z@leavevmode{\ifvmode\if@inlabel\indent\else\if@noskipsec\indent\else + \if@nobreak\global\@nobreakfalse\everypar={}\fi + {\parskip=0pt\noindent}\fi\fi\fi} +% \end{macrocode} +% +% extra vertical space in non-box environments +% +% \begin{macrocode} +\def\also{\crcr\noalign{\vskip\jot}} +\def\Also{\crcr\noalign{\vskip2\jot}} +\def\ALSO{\Also\Also} +% \end{macrocode} +% +% extra vertical space in boxed environments +% +% \begin{macrocode} +\def\als@{\crcr\@but\omit\vrule height\jot width\zedlinethickness \cr \@but} +\def\Als@{\crcr\@but\omit\vrule height2\jot width\zedlinethickness \cr \@but} +\def\ALS@{\crcr\@but\omit\vrule height4\jot width\zedlinethickness \cr \@but} +% \end{macrocode} +% +%\subsection{Environment-breaking commands} +% +% \begin{macrocode} +\def\znewpage{\also\noalign{\penalty\forcepagepenalty}\also} +\def\zbreak{\also\noalign{\penalty\interdisplaylinepenalty\vskip-\jot}\also} +\def\Zbreak{\also\noalign{\penalty\interdisplaylinepenalty}\also} +\def\ZBREAK{\Also\noalign{\penalty\interdisplaylinepenalty}\Also} +\def\t#1{\hskip #1\zedtab} +%\def\c#1#2{\hbox to #1\zedtab{$#2$\hfil}} +\def\flushr#1{\crcr\quad\cr} +% \end{macrocode} +% +%\section{Utility macros for Object-Z} +% +% \begin{macrocode} +\def\z@inclasscheck{\ifz@inclass\else + \@latexerr{This Z environment is only allowed within a class} +{Perhaps you forgot to include a \string\begin\string{class\string} +somewhere^^Jor you are trying to print a file that needs updating.^^J\@ehc} \fi} +\def\z@outclasscheck{\ifz@inclass + \@latexerr{This Z environment is not allowed inside a class} +{This environment doesn't really make sense within a class.^^J% +If you really want it then I'll try my best to fit in in.^^J\@ehc}\else +\ifz@inenv \@latexerr{New Z environment declared before previous +one is completed} +{I suspect that you've forgotten to finish the last environment.^^J% +You are trying to nest environments and this can only be done inside classes^^J% +besides, the environment you have started isn't valid within classes any way.^^JI suggest that you type \space X \space to quit and then correct your document.} +\fi\fi} +% +\def\z@makeouter{% + \ifz@inenv + \ifz@inclass\z@inenvfalse + \hskip-\zedleftsep \advance\linewidth by -\zedlinethickness + \zedindent=\zedleftsep \zedleftsep=0.8\zedleftsep + \zedbar=0.8\zedbar \zedtab=0.8\zedtab + \oz@parbox{\linewidth}\bgroup + \z@zeroskips + \else + \@latexerr{Incorrect place for Z environment; nesting is + allowed only inside classes} + {You've either forgotten to finish the last environment,^^J% + you've forgotten to include a + \string\begin\string{class\string} somewhere^^J% + or you are trying to print a file that needs updating.^^J% + (Then again, you might just be trying to do something^^J% + that the author of these macros didn't intend you to do)^^J\@ehc} + \fi + \else + \bgroup + \fi +} +% +\def \z@makeinner{\egroup + \global\z@curindent\z@ +} +% +\def \classbreak{\also\egroup$$\vskip -\ht\zstrutbox + \vskip -\abovedisplayskip\vskip -\belowdisplayskip\z@wide\z@boxenv\also} +% \end{macrocode} +% +%\section{Non-box environments} +% +% +% ZED for non-box multiline formulas +% +% \begin{macrocode} +\def\zed{\z@outnonbox\z@inboxfalse\z@format} +\def\endzed{\crcr\egroup\endz@env} +\let\[=\zed +\def\]{\crcr\egroup$$\ignorespaces} +% \end{macrocode} +% +% ARGUE for algebraic arguments +% +% used for algebraic proofs expressed as extended equations. +% like zed but with extra spacing between lines +% Generates an alignment display, which may be split across pages. +% +% \begin{macrocode} +\def\argue{\z@outnonbox\interzedlinepenalty=\interdisplaylinepenalty + \openup 1\jot \z@format + \noalign{\vskip-\jot}}% equal vspace above and below argue display +\let\endargue=\endzed +% \end{macrocode} +% +% INFRULE for inference rules +% +% used for inference rules. The horizontal line is generated by |\derive|: +% an optional argument contains the side-conditions of the rule. +% +% \begin{macrocode} +\def\infrule{\z@outnonbox\halign\bgroup + \zstrut\quad$\@lign##$\quad\hfil&\quad\@lign##\hfil\cr} +\let\endinfrule=\endzed +\def\derive{\crcr\also\@but\omit\z@hrulefill% + \@ifnextchar[{\z@sidecondition}{\cr\also\@but}} +\def\Derive{\crcr\also\@but\omit\z@hrulefill\cr\@but + \noalign{\kern-\dp\zstrutbox + \kern\doublerulesep \nobreak}% +\omit\derive} +\def\z@sidecondition[#1]{&$\smash{\lower 0.2ex\hbox{$[\;#1\;]$}}$\cr\also\@but} +% \end{macrocode} +% +% SYNTAX for syntax rules +% +% `syntax' environment: used for syntax rules --- even (once!) for VDM. +% \begin{macrocode} +\def\syntax{\z@outnonbox\halign\bgroup + \zstrut$\@lign##$\hfil &\hfil$\@lign{}##{}$\hfil + &$\@lign##$\hfil &\qquad\@lign-- ##\hfil\cr} +\let\endsyntax=\endzed +% \end{macrocode} +% +% \subsection{Boxed environments} +% +% +% SCHEMA schema definitions +% +% \begin{macrocode} +\def\schema#1{\z@inoutbox\z@topline{$\,#1\,$}} +\def\endschema{\z@botline \endzed \z@makeinner \z@nopar} +% \end{macrocode} +% +% ANONSCHEMA schema with no name +% +% \begin{macrocode} +\@namedef{anonschema}{\leftnamesfalse\z@inoutbox\z@topline{}} +\expandafter\let\csname endanonschema\endcsname=\endschema +% \end{macrocode} +% +% GENSCHEMA generic schema definitions +% +% \begin{macrocode} +\def\genschema#1#2{\z@inoutbox\z@topline{$\,#1\:[#2]\,$}} +\let\endgenschema=\endschema +% \end{macrocode} +% +% AXDEF `liberal' axiomatic definitions +% +% \begin{macrocode} +\def\axdef{\z@inoutbox} +\def\endaxdef{\endzed\z@makeinner} +% \end{macrocode} +% +% UNIQDEF `unique' axiomatic definitions +% +% \begin{macrocode} +\def\uniqdef{\leftnamesfalse\z@inoutbox\z@dbltopline{}} +\let\enduniqdef=\endschema +% \end{macrocode} +% +% GENDEF 'generic' axiomatic definitions +% +% HACK TO MAKE IT COMPATIBLE WITH FUZZ.STY +% \begin{macrocode} +\def\gendef{\@ifnextchar[{\z@gendef}{\z@@gendef}} +\def\z@gendef[#1]{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,[#1]\,$}} +\def\z@@gendef#1{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,[#1]\,$}} +\let\endgendef=\endschema +% \end{macrocode} +% +% GENGENDEF generic contents 'generic' axiomatic definitions +% +% Hack to provide syntax-oriented display boxes +% \begin{macrocode} +\def\gengendef{\@ifnextchar[{\z@gengendef}{\z@@gengendef}} +\def\z@gengendef[#1]{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,#1\,$}} +\def\z@@gengendef#1{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,#1\,$}} +\let\endgengendef=\endschema +% \end{macrocode} +% +% CLASS +% +% \begin{macrocode} +\def\class#1{\z@leavevmode\z@makeouter\z@inclasstrue + \z@boxenv\z@topline{$\,#1\,$}} +\let\endclass\endschema +% \end{macrocode} +% +% OP +% +% \begin{macrocode} +\def\op{\z@inclasscheck\schema} +\let\endop\endschema +% \end{macrocode} +% +% STATE +% +% \begin{macrocode} +\def\state{\z@inclasscheck\anonschema} +\let\endstate\endschema +% \end{macrocode} +% +% INIT +% +% \begin{macrocode} +\def\init{\z@inclasscheck\schema{\Init}} +\let\endinit\endschema +% \end{macrocode} +% +% CONST +% +% \begin{macrocode} +\let\const\axdef +\let\endconst\endaxdef +% \end{macrocode} +% +% TYPE +% +% \begin{macrocode} +\def\type{\z@inclasscheck} +\let\endtype\relax +% \end{macrocode} +% +%\subsection{Other environments} +% +% SIDEBYSIDE +% +% This should support an arbitary number of columns +% |\zedindent|'s proportion of |\linewidth| gives a practical limit +% +% \begin{macrocode} +\def\sidebyside{\@ifnextchar[{\z@columns}{\z@columns[2]}} +\def\z@columns[#1]{\z@leavevmode\z@cols#1 \z@makeouter\z@narrow% + $$\lineskip=0pt\z@incolstrue + \predisplaysize\maxdimen + \ifz@leftmargin\hskip-\zedindent\z@leftmarginfalse\fi + \setbox0=\hbox to \linewidth\bgroup\z@zeroskips% + \divide\zedbar by \z@cols \divide\zedleftsep by \z@cols + \divide\zedtab by \z@cols \divide\linewidth by \z@cols + \oz@parbox[t]{\linewidth}\bgroup\z@wide} +% +\def\nextside{\egroup\hss\oz@parbox[t]{\linewidth}\bgroup\z@wide} +% +\newdimen\z@temp +\def\endsidebyside{\egroup\egroup + \z@temp\ht0 \advance\z@temp by \dp0\advance\z@temp by-\dp\zstrutbox + \hbox{\raise\z@temp\box0}\endz@env\z@makeinner\z@nopar} +% \end{macrocode} +% +% ZPAR +% +% \begin{macrocode} +\def\zpar{\z@leavevmode + \ifz@inenv\z@inclasstrue\fi% fudge to let zpar in all boxes + \z@makeouter\z@changesize + \advance\linewidth by -\z@curindent + \advance\linewidth by -\wd\z@curline + \hskip-\wd\z@curline\advance\linewidth by -\zedindent$$ + \ifz@leftmargin\hskip-\zedindent\fi% adjustment for first column + \advance\displayindent by \zedindent + \advance\displaywidth by -\zedindent + \advance\displayindent by \z@curindent + \advance\displayindent by \wd\z@curline + \advance\displaywidth by -\z@curindent + \advance\displaywidth by -\wd\z@curline + \global\setbox\z@curline\hbox{} + \z@narrow\oz@parbox[b]{\linewidth}\bgroup\hfil\break} +\def\endzpar{\egroup$$\z@makeinner\z@nopar} +% \end{macrocode} +% +% CLASSCOM +% +% \begin{macrocode} +\def \classcom{\zpar\sf} +\let \endclasscom=\endzpar +% \end{macrocode} +% +% PROOF +% +% \begin{macrocode} +\def\proof{\zpar$\PR$\zpar} +\def\endproof{\endzpar\endzpar} +% \end{macrocode} +% +% Additional auxiliary macros +% +% \begin{macrocode} +\def\zseq#1{\lseq #1 \rseq} +\def\zset#1{\{ #1 \}} +\def\zimg#1{\limg #1 \rimg} +\def\zsch#1{\lsch #1 \rsch} +\def\zimgset#1{\zimg\zset{#1}} +% \end{macrocode} +% +% OZ FUZZ +% +% |\defs| == +% |\sdef| |\defs| +% +% \begin{macrocode} +\def\fuzzcompatible{% +\let\defs\sdef +\let\empty\emptyset +} +% +% +% \end{macrocode} +% \Finale +\endinput diff --git a/Master/texmf-dist/source/latex/objectz/oz.ins b/Master/texmf-dist/source/latex/objectz/oz.ins new file mode 100644 index 00000000000..5e8ce211677 --- /dev/null +++ b/Master/texmf-dist/source/latex/objectz/oz.ins @@ -0,0 +1,53 @@ +% \iffalse +% LaTex2e Oz style for typesetting Object Z +% \fi +\def\fileversion{1} +\def\filedate{1993/12/23} +% +% \StopEventually{} +% +% As always we begin by identifying the latest version of this file +% on the VDU and in the {\sf log} file. +% \begin{macrocode} +\def\batchfile{oz.ins} +\input docstrip.tex +\preamble + +Copyright (C) 1993 by Sebastian Rahtz +All rights reserved. + +This file is part of the PSNFSS2e package. +\endpreamble + +\def\batchfile{oz.dst} % ignored in distribution +\input docstrip.tex % ignored in distribution + +\keepsilent + +\preamble +Copyright (C) 1993 Sebastian Rahtz. All rights reserved. +This is a generated file for Object Z. Permission is granted to to +customize the declarations in this file to serve the needs of your +installation. However, no permission is granted to distribute a +modified version of this file under its original name. + +\endpreamble + +\Msg{*** Generating style file for Oz ***} + +\generateFile{oz.sty}{f}{ + \from{oz.dtx}{package}} + + +\Msg{***********************************************************} +\Msg{*} +\Msg{* To finish the installation you have to move the} +\Msg{* file oz.sty into a directory searched by TeX} +\Msg{*} +\Msg{***********************************************************} + + +\endinput + + + diff --git a/Master/texmf-dist/source/latex/objectz/readme b/Master/texmf-dist/source/latex/objectz/readme new file mode 100644 index 00000000000..c3ee8cd92f9 --- /dev/null +++ b/Master/texmf-dist/source/latex/objectz/readme @@ -0,0 +1,45 @@ +This is a revision of Paul King's oz.sty macros for typesetting Object Z, +updated for LaTeX2e. Users should run ozguide.tex through \LaTeX\ (after +installation!) for details of usage. + +Install by running \TeX\ on oz.ins and install oz.sty where \LaTeX\ +can find it. + +UPDATE NOVEMBER 1996 +******************** + +The Formal Methods Group in the Computer Science Department at the +University of Queensland recently released 'wizard', a type checker +for Object-Z specifications. Included in the wizard release was an +updated version of the oz.sty file for LaTeX 2.09. + +I have implemented all changes made in the oz.sty for LaTeX 2.09, +since it's last official release in late 1990, into the oz.dtx file +which you maintain for LaTeX 2e. I have attached my updated version +of oz.dtx to this message so that you may check these modifications +and officially release the updated version. + +The changes were made to the oz.dtx file with last changes logged +on 22 Feb 95 (this is the version currently available from CTAN). +All modifications and additions I have made are clearly indicated in +the updated file for your convenience. + +Should you need to compare my changes with the updated oz.sty file for +LaTeX 2.09, you can download the wizard archive from the following url: + + ftp://ftp.cs.uq.edu.au/pub/SVRC/software/wizard.tar.gz + +The new oz.sty file and oz.tex file are located in the wizard/tex +subdirectory when the archive is extracted. + +Please contact me if you need to. + +Thanks. + +Dave. +-- +David Leadbetter Email: davidl@cs.uq.edu.au +PhD Student Phone: + 61 7 3365 1204 +Department of Computer Science FAX: + 61 7 3365 1999 +The University Of Queensland 4072 AUSTRALIA + -- cgit v1.2.3