Initial commit

2 files changed, 720 insertions, 0 deletions

diff --git a/macros/latex209/contrib/zed/zed.sty b/macros/latex209/contrib/zed/zed.sty
new file mode 100644
index 0000000000..3990dab6f2
--- /dev/null
+++ b/macros/latex209/contrib/zed/zed.sty
@@ -0,0 +1,323 @@
+%LaTeX style
+%
+% zed.sty 15 feb 88
+%
+\typeout{Style Option 'zed'. Released 15 February 1988}
+
+%
+% Copyright (c) J.M. Spivey 1988
+%
+% This file contains a collection of macros for typesetting
+% Z specifications. There are four sections.
+%
+% 0. The mathcodes for letters are changed so that they generate text
+%    italic instead of math italic. This makes multi-letter identifiers
+%    look neater.
+%
+% 1. Environments for putting the maths in boxes.
+%
+% 2. Extra symbol fonts are loaded.
+%
+% 3. Mnemonics for Z symbols are defined. Note that certain plain TeX
+%    names are usurped here: \forall is made into a \mathop to give a
+%    thin space between it and the following declaration. The same goes
+%    for \lambda and \mu, and \exists.
+%
+
+%
+% Changes since 25 aug 87
+%
+% 25 aug 87	Renamed \tad as \also and \also as \zbreak. \def'ed \tad
+%		to \also for upward compatibility.
+%		Inserted message on loading.
+%
+% 15 sep 87	Revamped special symbol names.
+%
+% 18 sep 87	Changed \z@d to allow Z text in lists. 
+%
+% 24 sep 87	Removed assignment to \prevdepth from \endschema
+%		--- giving a little more vertical space.
+%
+%  8 oct 87	Removed a spurious space from \schema --- caused
+%		empty paragraph between adjacent schemas.
+%		Merged left bar code into \axdef. Removed redef
+%		of \_.
+%
+% 12 oct 87	Removed \@zedwidth -- use \linewidth instead.
+%		Removed a spurious space from \z@dpream.
+%
+% 16 oct 87	Removed def of \par from \z@d.
+%
+% 10 dec 87	Removed spurious space from \gendef
+%
+% 15 jan 88	Split into two parts to allow both AMS and OXSY versions.
+%
+% 15 feb 88	Added gendef* environment
+
+%
+% MATHCODES
+%
+% 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.
+%
+% 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.
+%
+
+\def\@setmcodes#1#2#3{{\count0=#1 \count1=#3
+	\loop \global\mathcode\count0=\count1 \ifnum \count0<#2
+	\advance\count0 by1 \advance\count1 by1 \repeat}}
+
+\@setmcodes{`A}{`Z}{"7441}
+\@setmcodes{`a}{`z}{"7461}
+
+\mathcode`\;="8000 % Makes ; active in math mode
+{\catcode`\;=\active \gdef;{\semicolon\;}}
+\mathchardef\semicolon="003B
+
+%
+% SCHEMAS, Etc.
+%
+% 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 (argue) may be split arbitrarily. All generate alignment
+% displays, and penalties are used to control page breaks.
+%
+\newdimen\zedindent	\zedindent=\leftmargini
+\newdimen\zedleftsep	\zedleftsep=1em
+\newdimen\zedtab	\zedtab=2em
+\newdimen\zedbar	\zedbar=6em
+\newcount\interzedlinepenalty \interzedlinepenalty=10000
+\newcount\preboxpenalty \preboxpenalty=0
+\newif\ifzt@p		\zt@pfalse
+
+\def\n@rrow{\advance\linewidth by-\zedindent}
+\def\t@pline#1{\omit \hbox to\linewidth{\strut
+	\leftt@p#1\thinspace\hrulefill}\cr}
+\def\z@dline{\omit \hbox to\linewidth{\hrulefill}\cr}
+\def\z@dpream{\halign to\linewidth\bgroup
+        \strut\z@dleft$\@lign##$\hfil \tabskip=0pt plus1fil%
+	&\hbox to0pt{\hss$\@lign##$}\tabskip=0pt\cr}
+\let\z@dleft=\relax
+
+\def\zbreak{\crcr \noalign{\penalty\interdisplaylinepenalty} \also}
+\def\also{\crcr \noalign{\vskip\jot}}
+\def\tad{\also}
+
+\def\@zed{\ifvmode\@zleavevmode\fi
+	$$\global\zt@ptrue \lineskip=0pt
+	\advance\linewidth by-\zedindent
+	\advance\displayindent by\zedindent
+	\def\\{\crcr}% Must have \def and not \let for nested alignments.
+	\everycr={\noalign{\ifzt@p \global\zt@pfalse
+		\else \penalty\interzedlinepenalty \fi}}
+        \tabskip=0pt}
+\def\end@zed{$$\global\@ignoretrue}
+
+\def\zed{\@zed\z@dpream}
+\def\endzed{\crcr\egroup\end@zed}
+
+\let\[=\zed
+\def\]{\crcr\egroup$$\ignorespaces}
+
+\def\axdef{\let\zbreak=\zbre@k \let\also=\@lso \let\z@dleft=\@zedleft
+	\predisplaypenalty=\preboxpenalty \zed}
+\let\endaxdef=\endzed
+\def\zbre@k{\also \noalign{\penalty\interdisplaylinepenalty \vskip-\jot} \also}
+\def\@lso{\crcr \@but \omit\vrule height\jot \cr \@but}
+\def\@zedleft{\vrule\hskip\zedleftsep}
+\def\@but{\noalign{\nointerlineskip}}
+
+\def\schema#1{\n@rrow\axdef \t@pline{$#1$}}
+\def\endschema{\also \z@dline \endzed}
+
+\def\where{\also \omit \hbox to\zedbar{\hrulefill}\cr \also}
+
+\@namedef{schema*}{\n@rrow\axdef
+	\noalign{\kern-\ht\strutbox} \z@dline \also}
+\expandafter\let\csname endschema*\endcsname=\endschema
+
+\def\gendef#1{\let\leftt@p=\@leftt@p
+        \setbox0=\hbox{$[#1]$}\setbox1=\null \wd1=\wd0
+        \n@rrow\axdef \t@pline{\box0}%
+        \noalign{\kern-\baselineskip\kern-\doublerulesep \nobreak}%
+	\t@pline{\box1} \noalign{\kern\doublerulesep \nobreak}}
+\let\endgendef=\endschema
+
+\@namedef{gendef*}{\n@rrow\axdef
+	\noalign{\kern-\ht\strutbox} \z@dline
+	\noalign{\kern-\baselineskip\kern-\doublerulesep \nobreak}
+	\z@dline \noalign{\kern\doublerulesep \nobreak} \also}
+\expandafter\let\csname endgendef*\endcsname=\endschema
+
+% `infrule' environment: used for inference rules. The horizontal line is
+% generated by \derive: an optional argument contains the side-conditions
+% of the rule.
+\def\infrule{\@zed \halign\bgroup
+	\strut\quad$\@lign##$\quad\hfil&\quad\@lign##\hfil\cr}
+\let\endinfrule=\endzed
+
+\def\derive{\crcr\also\@but\omit\hrulefill\@ifnextchar[{\@xderive}{\@yderive}}
+\def\@xderive[#1]{&$\smash{\lower 0.5ex\hbox{$[\;#1\;]$}}$\cr\also\@but}
+\def\@yderive{\cr\also\@but}
+
+% `argue' environment: used for algebraic proofs expressed as extended
+% equations. Generates an alignment display, which may be split across
+% pages.
+\def\argue{\@zed \interzedlinepenalty=\interdisplaylinepenalty
+	\openup 1\jot \z@dpream \noalign{\vskip-\jot}}
+\let\endargue=\endzed
+
+% `syntax' environment: used for syntax rules - even (once!) for VDM.
+\def\syntax{\@zed \halign\bgroup
+	\strut$\@lign##$\hfil &\hfil$\@lign{}##{}$\hfil
+	&$\@lign##$\hfil &\quad\@lign-- ##\hfil\cr}
+\let\endsyntax=\endzed
+
+\def\@leftt@p{\vrule height0.4pt\hbox to\zedleftsep{\hrulefill\thinspace}}
+\let\leftt@p=\@leftt@p
+\def\leftschemas{\let\leftt@p=\relax}
+
+\def\t#1{\hskip #1\zedtab}
+\def\flushr#1{\crcr&#1\quad\cr}
+
+% \@zleavevmode -- Enter horizontal mode, taking account of possible
+% interaction with lists and section heads:
+%	1	After a \item, use \indent to get the label (this
+%		fails to run in even short labels).
+%	2	After a run-in heading, use \indent.
+%	3	After an ordinary heading, throw away the \everypar
+%		tokens, reset \@nobreak, and use \noindent with \parskip
+%		zero.
+%	4	Otherwise, use \noindent with \parskip zero
+\def\@zleavevmode{\if@inlabel\indent\else\if@noskipsec\indent\else
+	\if@nobreak\global\@nobreakfalse\everypar={}\fi
+	{\parskip=0pt\noindent}\fi\fi}
+
+%
+% FONTS
+%
+% The AMS extra symbol fonts are loaded.
+%
+
+\def\@fontname{\ifcase\@ptsize m10 scaled \@m%
+\or m10 scaled \magstephalf%
+\or m10 scaled \magstep1%
+\else m\@ptsize\fi}
+\font\msx=msx\@fontname % Note: sometimes called euxm10
+\font\msy=msy\@fontname % Note: sometimes called euym10
+
+\newfam\msxfam \textfont\msxfam=\msx
+\newfam\msyfam \textfont\msyfam=\msy
+
+\def\@famletter#1{\ifcase #1 0\or 1\or 2\or 3\or 4\or 5\or 6\or 7\or
+	8\or 9\or A\or B\or C\or D\or E\or F\fi}
+
+\edef\@fx{\@famletter\msxfam}
+\edef\@fy{\@famletter\msyfam}
+
+\def\bbold{\fam\msyfam \msy}
+
+%
+% Z SYMBOLS
+%
+
+\def\token#1{\hbox{`$#1$'}} % makes a quoted expression in mathematical text
+
+\def\report#1{\hbox{`{\tt #1}'}} % used for error messages in Z specs
+
+% \@myop makes an operator, with a strut to defeat TeX's vertical adjustment.
+\def\@myop#1{\mathop{\mathstrut{#1}}\nolimits}
+
+% This underscore doesn't have the little kern --- you get an italic
+% correction anyway in math mode.
+\def\_{\leavevmode \vbox{\hrule width0.5em}}
+
+% Save \q as \xq for quantifiers q.
+\let\xforall=\forall
+\let\xexists=\exists
+\let\xlambda=\lambda
+\let\xmu=\mu
+
+% \p and \f make arrows with 1 and 2 crossings resp.
+\def\p#1{\mathrel{\ooalign{\hfil$\mapstochar\mkern 5mu$\hfil\cr$#1$}}}
+\def\f#1{\mathrel{\ooalign{\hfil
+	$\mapstochar\mkern 3mu\mapstochar\mkern 5mu$\hfil\cr$#1$}}}
+
+\let\@mc=\mathchardef
+
+% In the same order as the Z reference manual ...
+
+% Chapter 1
+\def \lblot	{\langle\!\left|}
+\def \rblot	{\right|\!\rangle}
+
+% Chapter 2
+\def \defs	{\mathrel{\widehat=}}
+\def \power	{\@myop{\bbold P}}
+\let \cross	\times
+\def \lambda	{\@myop{\xlambda}}
+\def \mu	{\@myop{\xmu}}
+\def \lbag	{[\![}
+\def \rbag	{]\!]}
+\def \lnot	{\neg\;}
+\def \land	{\mathrel{\wedge}}
+\def \lor	{\mathrel{\vee}}
+\let \implies	\Rightarrow
+\let \iff	\Leftrightarrow
+\def \forall	{\@myop{\xforall}}
+\def \exists	{\@myop{\xexists}}
+\def \spot	{\mathrel{\bullet}}
+\def \hide	{\mathrel{\backslash}}
+\@mc \project	"3\@fx16
+\def \pre	{\@myop{\rm pre}}
+\def \semi	{\mathrel{\comp}}
+\def \ldata	{\langle\!\langle}
+\def \rdata	{\rangle\!\rangle}
+\def \shows	{\;\vdash\;}
+
+% Chapter 3
+\@mc \empty	"0\@fy3F
+\let \rel	\leftrightarrow
+\def \dom	{\@myop{\rm dom}}
+\def \ran	{\@myop{\rm ran}}
+\def \id	{\@myop{\rm id}}
+\def \comp	{\mathbin{\raise 0.6ex\hbox{\oalign{\hfil$\scriptscriptstyle
+		 \rm o$\hfil\cr\hfil$\scriptscriptstyle\rm 9$\hfil}}}}
+\@mc \dres	"2\@fx43
+\@mc \rres	"2\@fx42
+\def \ndres	{\mathbin{\rlap{$-$}{\dres}}}
+\def \nrres	{\mathbin{\rlap{$-$}{\rres}}}
+\def \limg	{(\!\left|}
+\def \rimg	{\right|\!)}
+\def \pfun	{\p\fun}
+\let \fun	\rightarrow
+\def \pinj	{\p\inj}
+\@mc \inj	"3\@fx1A
+\def \psurj	{\p\surj}
+\def \surj	{\mathrel{\ooalign{$\fun$\hfil\cr$\mkern4mu\fun$}}}
+\def \bij	{\mathrel{\ooalign{$\inj$\hfil\cr$\mkern5mu\fun$}}}
+\def \nat	{{\bbold N}}
+\def \num	{{\bbold Z}}
+\def \div	{\mathbin{\rm div}}
+\def \mod	{\mathbin{\rm mod}}
+\def \upto	{\mathbin{\ldotp\ldotp}}
+\def \finset	{\@myop{\bbold F}}
+\def \ffun	{\f\fun}
+\def \finj	{\f\inj}
+\def \seq	{\@myop{\rm seq}}
+\def \cat	{\mathbin{\raise 0.8ex\hbox{$\mathchar"2\@fx61$}}}
+\@mc \filter	"2\@fx16
+\def \dcat	{\@myop{\cat/}}
+\def \disjoint  {{\rm disjoint}\;}
+\def \partition {\mathrel{\rm partition}}
+\def \bag	{\@myop{\rm bag}}
+\def \inbag     {\mathrel{\rm in}}
diff --git a/macros/latex209/contrib/zed/zmacros.tex b/macros/latex209/contrib/zed/zmacros.tex
new file mode 100644
index 0000000000..5e6f0b0d24
--- /dev/null
+++ b/macros/latex209/contrib/zed/zmacros.tex
@@ -0,0 +1,397 @@
+% ZMACROS.TEX		Mike Spivey	July 1987
+\documentstyle[palatino,11pt,zed]{article}
+\begin{document}
+\title{Printing Z with \LaTeX}
+\author{Mike Spivey}
+\date{15th September 1987}
+\maketitle
+
+\section{Introduction}
+
+This note describes a small package of \LaTeX\ macros for printing
+Z specifications.
+I put these together specifically for printing my book on Z semantics,
+so the package only provides features I needed for that, and your
+favourite Z constructs may be missing.
+On the other hand, I've put quite a lot of work into getting
+the constructs which {\em are\/} there to look right, at
+least to my eyes. If the package doesn't do what you want,
+at least it gives you something to start from.
+The package does several related things for you:
+\begin{enumerate}
+\item   It loads the two fonts of extra symbols from the American
+        Mathematical Society and defines mnemonics for the Z symbols
+        they contain.
+\item   It defines macros to fudge some Z symbols (e.g. $\pinj$) which
+        don't appear in any of our fonts.
+\item   It fixes the way \TeX\ sets letters in mathematical formulas so
+        that multi-character identifiers look better.
+\item   It provides ways to set the various brands of `boxed mathematics'
+        which appear in Z specifications.
+\end{enumerate}
+
+\section{Loading the macros}
+
+The package is kept in a file {\tt zed.sty}, so to load it at
+the start of a \LaTeX\ run, you just begin with
+\begin{quote}
+\begin{verbatim}
+\documentstyle[11pt,zed]{article}
+\end{verbatim}
+\end{quote}
+or something like it.
+At PRG, the package only works with the eleven-point base size at
+present: the extra-symbols fonts it loads are only available at
+this size on the LBP--10.
+
+\section{The care and feeding of schemas}
+
+To print the schema
+\begin{schema}{PhoneDB}
+    known: \power NAME \\
+    phone: NAME \pfun PHONE
+\where
+    known = \dom phone
+\end{schema}
+you just say
+\begin{quote}
+\begin{verbatim}
+\begin{schema}{PhoneDB}
+    known: \power NAME \\
+    phone: NAME \pfun PHONE
+\where
+    known = \dom phone
+\end{schema}
+\end{verbatim}
+\end{quote}
+What could be simpler?
+If you want a schema with no name, just a horizontal rule at the top,
+use the \verb|schema*| environment instead.
+In fact, here is an example:
+% \begin{schema*}
+%	known: \power NAME \\
+%	phone: NAME \pfun PHONE
+% \where
+%	known = \dom phone
+% \end{schema*}
+If you like the name set flush left, you can use the \verb|\leftschemas|
+declaration to get the following effect:
+\begin{leftschemas}
+\begin{schema}{PhoneDB}
+    known: \power NAME \\
+    phone: NAME \pfun PHONE
+\where
+    known = \dom phone
+\end{schema}
+\end{leftschemas}
+As well as these, there's \verb|axdef|
+for axiomatic definitions: to print
+\begin{axdef}
+    policy: \power_1 RESOURCE \fun RESOURCE
+\where
+    \forall S: \power_1 RESOURCE \spot \\
+\t1         policy(S) \in S,
+\end{axdef}
+you say
+\begin{quote}
+\begin{verbatim}
+\begin{axdef}
+    policy: \power_1 RESOURCE \fun RESOURCE
+\where
+    \forall S: \power_1 RESOURCE \spot \\
+\t1         policy(S) \in S,
+\end{axdef}
+\end{verbatim}
+\end{quote}
+The strange hint \verb|\t1| in this example makes the corresponding
+line in the output have one helping of indentation.
+As things get more nested, you can say \verb|\t2|, \verb|\t3|, and so on.
+But if you should ever get beyond \verb|t9|, you'll need to use braces
+around the argument: \verb|\t{10}|, and you'd better look for some way
+to simplify your specification!
+The syntax of these little tab marks is a bit strange, I'm afraid,
+but I find them more convenient than other possibilities. They're short,
+and they don't get longer as the tabbing gets deeper, within reason,
+so they can be tucked in neatly on the left, well away from the
+maths.
+The size of `helping' you get with \verb|\t| is a parameter
+\verb|\zedindent|, and the default is 2em.
+
+Two other things to notice here are the little space between the
+$\forall$ and the following $S$, and the use of \verb|\spot| for
+the bullet $\spot$.
+These macros produce symbols of the right type for \TeX's spacing
+rules to insert spaces automatically.
+
+For generic definitions, there's the \verb|gendef| environment:
+you can get a neat double-topped box like
+\begin{gendef}{I,X,Y}
+    map: (X \pfun Y) \fun (I \pfun X) \fun (I \pfun Y)
+\where
+    map\,f = \lambda s: I \pfun X \mid
+        \ran s \subseteq \dom f \spot f \circ s
+\end{gendef}
+by typing
+\begin{quote}
+\begin{verbatim}
+\begin{gendef}{I,X,Y}
+    map: (X \pfun Y) \fun (I \pfun X) \fun (I \pfun Y)
+\where
+    map\,f = \lambda s: I \pfun X \mid
+        \ran s \subseteq \dom f \spot f \circ s
+\end{gendef}
+\end{verbatim}
+\end{quote}
+You should take note of the thin space I've inserted between $map$ and $f$
+in this example: if this is omitted, the input \verb|map f| gives
+$map f$, because \TeX\ ignores spaces in math mode.
+There's also a \verb|gendef*| environment for generic definitions with no
+parameters.
+
+If a schema or other box contains more than one predicate below the
+line, it often looks better to add a tiny vertical space between
+them, as in this example:
+\begin{schema}{AddPhone}
+    \Delta PhoneDB \\
+    name?: NAME \\
+    number?: PHONE
+\where
+    name? \notin known
+\also
+    phone' = phone \oplus \{name? \mapsto number?\}
+\end{schema}
+This is done with the command \verb|\also|, which behaves syntactically
+like \verb|\where|:
+\begin{quote}
+\begin{verbatim}
+\begin{schema}{AddPhone}
+    \Delta PhoneDB \\
+    name?: NAME \\
+    number?: PHONE
+\where
+    name? \notin known
+\also
+    phone' = phone \oplus \{name? \mapsto number?\}
+\end{schema}
+\end{verbatim}
+\end{quote}
+Note that \verb|\also| is provided {\em instead\/} of the
+optional argument to \verb|\\|
+which \LaTeX\ provides in other environments.
+
+\section{Other mathematical displays}
+
+The \verb|zed| environment can be used to set multi-line formulas without
+an enclosing box: it is useful for given-set declarations, theorems, and the
+miscellaneous bits of mathematics that don't come in a box:
+\begin{zed}
+    \forall n: \nat \spot \\
+\t1         n+n \in even.
+\end{zed}
+is printed from the input
+\pagebreak[3]
+\begin{quote}
+\begin{verbatim}
+\begin{zed}
+    \forall n: \nat \spot \\
+\t1         n+n \in even.
+\end{zed}
+\end{verbatim}
+\end{quote}
+The formula \verb|\begin{zed} ... \end{zed}| may be abbreviated to
+\verb|\[ ... \]|; the \verb|zed| environment is a generalization of the
+\verb|displaymath| environment of \LaTeX, so this redefinition of
+commands is fairly benign. Notice that the maths is set flush left on the
+same indentation as schemas and their friends.
+Here too you can use \verb|\also| for a little extra space
+between lines.
+
+For algebraic-style proofs, there is the \verb|argue| environment.
+This is like the \verb|zed| environment, but the separation between
+lines is increased a little, and page breaks may occur between lines.
+The intended use is for arguments like this:
+\begin{argue}
+    rev(append(cons(x,s),t)) \\
+\t1     = rev(cons(x,append(s,t))) \\
+\t1     = append(rev(append(s,t)),cons(x,nil)) \\
+\t1     = append(append(rev(t),rev(s)),cons(x,nil))
+                \quad \hbox{by hypothesis} \\
+\t1     = append(rev(t),append(rev(s),cons(x,nil))) \\
+\t1     = append(rev(t),rev(cons(x,s))).
+\end{argue}
+Here, again, is the input:
+\begin{quote}
+\begin{verbatim}
+\begin{argue}
+    rev(append(cons(x,s),t)) \\
+\t1     = rev(cons(x,append(s,t))) \\
+\t1     = append(rev(append(s,t)),cons(x,nil)) \\
+\t1     = append(append(rev(t),rev(s)),cons(x,nil))
+                \quad \hbox{by hypothesis} \\
+\t1     = append(rev(t),append(rev(s),cons(x,nil))) \\
+\t1     = append(rev(t),rev(cons(x,s))).
+\end{argue}
+\end{verbatim}
+\end{quote}
+When the left-hand side is long, I find this style better than the
+\LaTeX\ \verb|eqnarray| style, which wastes a lot of space.
+
+Another brand of box is the inference rule; the rule
+\begin{infrule}
+    \Gamma \shows P
+\derive[x \notin freevars(\Gamma)]
+    \Gamma \shows \forall x \spot P
+\end{infrule}
+comes from the input
+\begin{quote}
+\begin{verbatim}
+\begin{infrule}
+    \Gamma \shows P
+\derive[x \notin freevars(\Gamma)]
+    \Gamma \shows \forall x \spot P
+\end{infrule}
+\end{verbatim}
+\end{quote}
+Note the optional argument to \verb|\derive|: it is a side-condition of
+the rule.
+
+Finally, there's the \verb|syntax| environment, used for
+making displays like this:
+\begin{syntax}
+    EXPR & ::= & IDENT      & identifier \\
+         &  |  & EXPR\;EXPR & application \\
+         &  |  & \lambda IDENT \spot EXPR
+                            & lambda-abstraction.
+\end{syntax}
+from input like this:
+\begin{quote}
+\begin{verbatim}
+\begin{syntax}
+    EXPR & ::= & IDENT      & identifier \\
+         &  |  & EXPR\;EXPR & application \\
+         &  |  & \lambda IDENT \spot EXPR
+                            & lambda-abstraction.
+\end{syntax}
+\end{verbatim}
+\end{quote}
+This kind of thing is useful when you're describing a language,
+and it can also be used for data-type definitions.
+I've even---time for a confession---used it once for a fragment
+of VDM\@.
+The final column is optional:
+just omit the third \verb|&| if you don't want it.
+
+\section{Inside the boxes}
+
+\makeatletter
+\def\nota{\interzedlinepenalty=\interdisplaylinepenalty
+        \@zed\halign\bgroup\strut\hbox to3em{$##$\hfil}\tabskip=0pt&##\hfil\cr}
+\let\endnota=\endzed
+\makeatother
+
+Now for the details of what you can put inside the boxes.
+The first thing to notice is that multi-letter identifiers look
+better than they do with vanilla \LaTeX: instead of
+$\mit specifications$, you get $specifications$.
+The letters haven't been spread apart, and the ligature $fi$ has been
+used.
+
+Almost all of the mathematical symbols of \LaTeX\ can be used, plus
+a few extra ones listed below.
+The mnemonics I've chosen may seem a little mad, but that's life.
+The \LaTeX\ symbols you can't use are the ones whose
+names have been redefined:
+mostly these are the same symbol, but with the spacing fixed for
+use in Z specifications.
+First, there are some new arrows, and some new names for old ones:
+\begin{nota}
+    \rel & \verb|\rel| \\
+    \fun & \verb|\fun| \\
+    \inj & \verb|\inj| \\
+    \surj & \verb|\surj| \\
+    \bij & \verb|\bij| \\
+    \implies & \verb|\implies| \\
+    \iff & \verb|\iff|
+\end{nota}
+There are also `accents' \verb|\p| and \verb|\f| which put one and two
+crossings repectively over the following arrow.
+So \verb|\p\fun| gives $\p\fun$ and (if you insist)
+\verb|\f\bij| gives $\f\bij$.
+There are also some new binary operations:
+\begin{nota}
+    \comp & \verb|\comp| \\
+    \dres & \verb|\dres| \\
+    \rres & \verb|\rres| \\
+    \ndres & \verb|\ndres| \\
+    \nrres & \verb|\nrres| \\
+    \cross & \verb|\cross| \\
+    \filter & \verb|\filter| \\
+    \upto & \verb|\upto| \\
+    \div & \verb|\div| \\
+    \mod & \verb|\mod| \\
+    \cat & \verb|\cat|
+\end{nota}
+and some new operators:
+\begin{nota}
+    \dom & \verb|\dom| \\
+    \ran & \verb|\ran| \\
+    \pre & \verb|\pre| \\
+    \id & \verb|\id| \\
+    \seq & \verb|\seq| \\
+    \bag & \verb|\bag| \\
+    \forall & \verb|\forall| \\
+    \exists & \verb|\exists| \\
+    \lambda & \verb|\lambda| \\
+    \mu & \verb|\mu| \\
+    \power & \verb|\power| \\
+    \finset & \verb|\finset| \\
+    \dcat & \verb|\dcat|
+\end{nota}
+The unique quantifier $\exists_1$ can be typeset as \verb|\exists_1|.
+There are a couple of new ordinary symbols:
+\begin{nota}
+    \empty & \verb|\empty| \\
+    \nat & \verb|\nat| \\
+    \num & \verb|\num|
+\end{nota}
+as well as a few fancy brackets:
+\begin{nota}
+    \limg\;\rimg & \verb|\limg \rimg| \\
+    \lbag\;\rbag & \verb|\lbag \rbag| \\
+    \ldata\;\rdata & \verb|\ldata \rdata| \\
+    \lblot\;\rblot & \verb|\lblot \rblot|
+\end{nota}
+Finally, the following bits and pieces come with the right spacing for Z:
+\begin{nota}
+    \land & \verb|\land| \\
+    \lor & \verb|\lor| \\
+    \lnot & \verb|\lnot| \\
+    \widehat= & \verb|\defs| \\
+    \hide & \verb|\hide| \\
+    \project & \verb|\project| \\
+    \semi & \verb|\semi| \\
+    \vdash & \verb|\shows| \\
+    \spot & \verb|\spot|
+\end{nota}
+Some of these are duplicates of binary operators listed above, but with
+names more appropriate to their use in schema-expressions; there is
+also a little more spacing in these variants.
+And that's about it.
+
+\section{Style parameters}
+
+\begin{description}
+\item[\tt\string\zedindent] The indentation for mathematical text.
+	By default, this is the same as \verb|\leftmargini|, the indentation
+	used for list environments.
+\item[\tt\string\zedleftsep] The space between the vertical line on the left
+	of schemas, etc., and the maths inside. The default is 1em.
+\item[\tt\string\zedtab] The unit of indentation used by \verb|\t|. The default
+	is 2em.
+\item[\tt\string\zedbar] The length of the horizontal bar in the middle of a
+	schema. The default is 6em.
+\item[\tt\string\leftschemas] A declaration which makes schema names be
+	set flush left. Use it in the document preamble.
+\end{description}
+
+\end{document}