doc 4

git-svn-id: svn://tug.org/texlive/trunk@80 c570f23f-e606-0410-a88d-b1316a301751

2 files changed, 1517 insertions, 0 deletions

diff --git a/Master/texmf-dist/doc/latex/objectz/ozguide.tex b/Master/texmf-dist/doc/latex/objectz/ozguide.tex
new file mode 100644
index 00000000000..9932d6dc0e4
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/objectz/ozguide.tex
@@ -0,0 +1,1311 @@
+\errorcontextlines=20
+\documentclass[a4paper]{article}
+\advance\textwidth by 1in
+\advance\textheight by 1in
+\advance\oddsidemargin by -0.5in
+\advance\topmargin by -0.5in
+\usepackage{oz}
+\usepackage{example}
+\usepackage{multicol}
+%
+% just ignore any over- or under-full hboxes
+% this document uses most of the (physical) page and isn't spread
+% out either.  This may make it slightly harder to read first time
+% through, but makes it more suitable for later reference.
+%
+% before we start, let's make a few definitions
+%
+\makeatletter
+%\def\example{\begin{sidebyside}}
+%\def\verbpart{\nextside\small\vspace*{-1ex}\begin{quote}\begin{verbatim}}
+%\def\endexample{\end{quote}\vspace*{-2ex}\end{sidebyside}\vspace*{-3ex}\ignorespaces}
+\def\symbol#1{#1 & \tt\string#1}
+\def\symbols{\@ifnextchar[{\@symbols}{\@symbols[0]}}
+\def\@symbols[#1]{\interzedlinepenalty=\interdisplaylinepenalty\z@env
+        \openup #1\jot
+        \halign\bgroup\zstrut\hbox to 3.8em{$##$\hss}\tabskip=0pt&##\hss\cr
+        \noalign{\vskip-#1\jot}}% equal vspace above and below argue display
+\let\endsymbols=\endzed
+\makeatother
+%
+\begin{document}
+\begin{center}
+{\Large\bf Printing Z and Object-Z \LaTeX\ documents}\\[2.5ex]
+{\em Paul King}\\[1ex]
+Department of Computer Science\\
+University of Queensland\\
+Australia, 4072\\
+king@batserver.cs.uq.oz.au\\[1ex]
+May 29, 1990
+\end{center}
+
+\section{Introduction}
+This note describes a package of \LaTeX\ macros for printing
+Z and Object-Z specifications.  The macros and this note are
+based originally on Mike Spivey's \verb'zed.sty' macros and documentation.
+The package does several related things for you:
+\begin{itemize}
+\item   It loads extra fonts and defines mnemonics
+        for the Z symbols they contain.
+\item   It defines macros for 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 various brands of `boxed mathematics'
+        which appear in Z and Object-Z specifications.
+\end{itemize}
+
+The package is kept in a file {\tt oz.sty}
+in the directory \verb|/usr/local/lib/tex/localinputs|.
+This directory should be mentioned in your \verb|TEXINPUTS| shell variable.
+To use the macros you just begin your \LaTeX\ document with something like:
+\begin{quote}
+\begin{verbatim}
+\documentstyle[11pt,oz]{article}
+\end{verbatim}
+\end{quote}
+\vspace*{-1.5ex}
+
+\section{Schema Boxes}
+
+The example below shows a schema on the left and what you
+need to say to get it on the right.
+
+\begin{example}
+\begin{schema}{BirthdayBook}
+    known: \pset NAME \\
+    birthday: NAME \pfun DATE
+\ST
+    known = \dom birthday
+\end{schema}
+\end{example}
+
+The command \verb|\ST| (read `Such That') is the same as the previously used
+command \verb|\where| which has been kept as an alias for upward compatibility.
+If you want a schema with no name, just a horizontal rule at the top,
+use the \verb|schema*| environment instead.
+You can set various parameters (see Section 7) to change the box style,
+for example:
+
+\begin{example}
+$BirthdayBook \sdef \lsch ... \rsch$
+\end{example}
+
+A generic schema is produced as follows.
+
+\begin{example}
+\begin{genschema}{Pool}{RESOURCE}
+owner : RESOURCE \pfun USER \\
+free : \pset RESOURCE
+\ST
+(\dom owner) \uni free = RESOURCE \\
+(\dom owner) \int free = \emptyset
+\end{genschema}
+\end{example}
+
+\section{Axiomatic definitions}
+
+A `liberal' axiomatic definition is produced as follows.
+
+\begin{example}
+\begin{axdef}
+limit : \nat
+\ST
+limit \leq 65536
+\end{axdef}
+\end{example}
+
+A `generic' axiomatic definition is produced as follows.
+
+\begin{example}
+\begin{gendef}{X,Y}
+first : X \prod Y \tfun X
+\ST
+\all x : X; y : Y \dot first(x,y) = x
+\end{gendef}
+\end{example}
+
+A `unique' axiomatic definition is produced as follows.
+
+\begin{example}
+\begin{uniqdef}
+\pi : \real
+\ST
+\pi = 3.14159265\ldots
+\end{uniqdef}
+\end{example}
+
+\section{Object-Z Class Boxes}
+
+Object-Z allows class types to be defined using a box very similar to
+the schema box previously described.  It allows the previously
+described boxed environments (as well as nested sub-classes) to be
+placed within a class box.  In addition, special names can be used for
+some of the boxed-environments when they appear within a class box.
+The following example illustrates a class definition.
+
+\begin{example}
+\begin{class}{Shape}
+\also
+colour : Colour \\
+\begin{axdef}
+perim : \real
+\ST
+perim > 0
+\end{axdef} \\
+\begin{classcom}
+This class has 2 constants
+$colour$ and $perim$.
+\end{classcom} \\
+\begin{state}
+x, y : \real
+\end{state} \\
+\begin{init}
+x = y = 0
+\end{init} \\
+\begin{op}{Translate}
+\Delta (x,y) \\
+dx?, dy? : \real
+\ST
+x' = x + dx? \\
+y' = y + dy?
+\end{op}
+\end{class}
+\end{example}
+
+The \verb|classcom| environment hasn't been seen before.
+It creates a paragraph of text with the same margins as used
+for schemas and other Z environments.  It uses a special font
+intended for use when placing comments inside classes.
+A similar environment, \verb|zpar|, uses the same margins
+but with the normal roman font.
+
+The \verb|\begin{init}| command is an abbreviation for
+\verb|\begin{schema}{\Init}|.  Similarly \verb|\begin{state}|
+is a more meaningful synonym for \verb|\begin{schema*}|.
+
+You will be given \LaTeX\ warning messages if you try to
+use a \verb|state| environment outside of a class box
+or if you try to place an environment such as \verb|syntax|
+inside a class.  You can ask for additional help in these
+cases using the normal \LaTeX\ \verb|h| or \verb|H| help commands.
+If you proceed with \LaTeX ing, the macros will attempt to
+do the best they can to do what you probably intend, even though
+you are violating the recommended nesting guidelines.
+
+\section{Controlling the Spacing within Equations and Boxes}
+
+Most of the special Z symbols are defined
+in a way that allows \TeX\ to space them out correctly.
+Sometimes, however, you'll need to give \TeX\ a helping hand if
+you want it to get the spacing right.  For example, to get $map\,f$
+you need to type \verb|map\,f|.  The \verb|\,| gives you a thin space:
+if this is omitted, the input \verb|map f| gives
+$map f$, because \TeX\ ignores spaces in math mode.
+
+Sometimes it is useful to indent the left margin to emphasis
+the logical structure of the predicate.
+The command \verb|\t1| does this by making 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!
+These little tab marks might look different to normal tabs
+but are never the less convenient. 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 determined by
+the \verb|\zedtab| parameter (see Section 7).
+
+If you want a more powerful aligning mechanism than tabbing
+then you can use the margin stack as shown in the example below.
+The command \verb|\M| sets the future left margin to the current
+horizontal position and pushes the old value onto a margin stack.
+The command \verb|\O| resets the left margin to its previous value
+(which is popped off the stack).
+
+\begin{example}
+\begin{schema}{Test}
+x, y : \nat
+\ST
+x + 1/x = 0 \imp \M y + 1/y = 0 \\
+y = x \O \\
+\end{schema}
+\end{example}
+
+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{example}
+\begin{schema}{AddBirthday}
+  \Delta BirthdayBook \\
+  n?: NAME \\
+  d?: DATE
+\ST
+  n? \nem known
+\also
+  birthday'=birthday \uni \{n? \map d?\}
+\end{schema}
+\end{example}
+
+This is done with the command \verb|\also|, which behaves syntactically
+like \verb|\ST|.
+The command \verb|\also| is provided {\em instead\/} of the
+optional argument to \verb|\\|
+which \LaTeX\ provides in other environments.
+If larger vertical spacing is required, the commands
+\verb|\Also| and \verb|\ALSO| may be used (giving 2 and 4 times
+as much space as \verb|\also| respectively).
+
+Normally, the contents of a schema box are kept on a single page.
+For large schemas it may be necessary to split the box across pages.
+You must specify which places are suitable for splitting using one of
+\verb|\zbreak|, \verb|\Zbreak| or \verb|\ZBREAK|.  If no split is
+performed at this point, a vertical space will be added as if the
+user had typed \verb|\also|, \verb|\Also|, or \verb|\ALSO| respectively.
+You can also use the \verb|\znewpage| command to force a page break within
+a box.  (These breaking facilities will hopefully never be needed for schemas,
+but may become necessary for class specifications.)
+
+\section{Other Display Environments}
+
+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:
+
+\vspace{-1ex}\begin{example}
+\begin{zed}
+    \all n: \nat \dot \\
+\t1         n+n \mem even.
+\end{zed}
+\end{example}
+
+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.
+When the left-hand side is long this style wastes less space
+than the \LaTeX\ \verb|eqnarray| style.
+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 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}
+
+The example below shows an inference rule (the optional argument
+to \verb|\derive| gives a side-condition of the rule):
+
+\vspace{-1ex}\begin{example}
+\begin{infrule}
+    \Gamma \shows P
+\derive[x \nem freevars(\Gamma)]
+    \Gamma \shows \all x \dot P
+\end{infrule}
+\end{example}
+
+The \verb|syntax| environment is used for making displays like this:
+
+\begin{syntax}
+  EXPR & \ddef & IDENT      & identifier \\
+       & \bbar & EXPR\;EXPR & application \\
+       & \bbar & \lambda IDENT \dot EXPR & lambda-abstraction.
+\end{syntax}
+from input like this:
+\begin{quote}
+\begin{verbatim}
+\begin{syntax}
+  EXPR & \ddef & IDENT                   & identifier \\
+       & \bbar & EXPR\;EXPR              & application \\
+       & \bbar & \lambda IDENT \dot 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 as shown below.
+The optional final column was omitted below by leaving out the third \verb|&|.
+
+\begin{example}
+\begin{syntax}
+TYPE & \ddef & givenT  \lang NAME \rang \\
+& \bbar & powerT \lang TYPE \rang \\
+& \bbar & tupleT \lang \seq TYPE \rang \\
+& \bbar & schemaT \lang IDENT \ffun TYPE \rang \\
+& \bbar & classT \lang IDENT \ffun ClassAttr \rang
+\end{syntax}
+\end{example}
+
+This can be compared with the layout adopted by the UQ Z editor (version 1).
+
+\begin{example}
+\begin{zed}
+TYPE \ddef \M givenT  \lang NAME \rang \\
+\bbar powerT \lang TYPE \rang \\
+\bbar tupleT \lang \seq TYPE \rang \\
+\bbar schemaT \lang IDENT \ffun TYPE \rang \\
+\bbar classT \lang IDENT \ffun ClassAttr \rang \O
+\end{zed}
+\end{example}
+
+The {\tt sidebyside} environment allows a display as shown in the
+first two columns below to be produced from the text of the third column.
+Note the use of the \verb|\comment| command.
+
+\begin{example}
+\begin{sidebyside}
+\begin{schema}{Schema}
+\comment*{declarations}
+\ST
+a < b \comment{pred-1} \\
+aaaaa < bbbbb \comment{pred-2}
+\end{schema}
+\nextside
+\begin{zpar}
+This is a paragraph which has the same
+margins as the standard schemas do.
+\end{zpar}
+\end{sidebyside}
+\end{example}
+
+In fact, this environment was used throughout this note to
+display the examples beside the required input text.
+Incidentally, the above example shows that \verb|sidebyside|
+environments can be nested; so what the author of this note typed
+to get the above display was:
+
+\begin{quote}
+\begin{verbatim}
+\begin{sidebyside}
+        \begin{sidebyside}
+                ...
+        \nextside
+                ...
+        \end{sidebyside}
+\nextside
+        ...
+\end{sidebyside}
+\end{verbatim}
+\end{quote}
+
+This resulted in the first two columns being equally spaced and
+together taking up as much space as the third column.
+You can have more than 2 columns without nesting by specifying an optional
+parameter to \verb|sidebyside|.  For example, the display below has three
+equally spaced columns obtained using \verb|\begin{sidebyside}[3]|.
+
+ \begin{sidebyside}[3]
+ \begin{schema}{BirthdayBook}
+     known: \pset NAME \\
+     birthday: NAME \pfun DATE
+ \ST
+     known = \dom birthday
+ \end{schema}
+ \nextside
+ \begin{schema}{BirthdayBook}
+     known: \pset NAME \\
+     birthday: NAME \pfun DATE
+ \ST
+     known = \dom birthday
+ \end{schema}
+ \nextside
+ \begin{zpar}
+Don't get carried away with \verb|sidebyside|
+ like this example does.
+ \end{zpar}
+ \end{sidebyside}
+ 
+\section{Style Parameters}
+
+\begin{description}
+\item[\tt\string\zedindent] The (horizontal) indentation for mathematical text.
+        By default, this is the same as \verb|\leftmargini|, the indentation
+        used for list environments.
+\item[\tt\string\zedleftsep] The (horizontal) 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 8em.
+\item[\tt\string\leftschemas] A declaration which makes schema names be
+        set flush left. Use it in the document preamble.
+\item[\tt\string\zedlinethickness] The thickness of the lines that make up
+        schema and class boxes.  You can change the thickness
+        with a command such as \verb|\zedlinethickness=0.1pt|.  This may
+        be useful if you are creating overhead slides.
+        \begin{description}
+        \makeatletter
+        \item[0.1pt] \zedlinethickness=0.1pt
+                ~\hbox to 4cm{\z@hrulefill}
+        \item[0.4pt] \zedlinethickness=0.4pt
+                ~\hbox to 4cm{\z@hrulefill}~~~(The default)
+        \item[\hphantom{0.}1pt] \zedlinethickness=1pt
+                ~\hbox to 4cm{\z@hrulefill}
+        \end{description}
+\item[\tt\string\baselinestretch] The spacing for the text part of your
+        document.  It doesn't change the spacing within Z environments.  It's
+        default value is 1.  A command such as \verb|\def\baselinestretch{2}|
+        will make your text double spaced, but not your Z environments.
+\item[\tt\string\zedbaselinestretch] The spacing for the Z environment
+        part of your document.  It's default value is 1.
+\item[\tt\string\zedsize] The size of the material within the Z
+        part of your document. It doesn't affect the remainder of your document.
+        For example, \verb|\zedsize{\large}| will give you large Z symbols
+        and equations but will not affect the size of the surrounding text.
+\item[\tt\string\zedcornerheight] The height of `corners' that can be placed
+        on the right hand side of the top and bottom lines of schema and class
+        boxes.  The default is 0em (i.e. no corners).
+\end{description}
+
+\section{Symbols}
+
+Multi-letter identifiers have been changed to look
+better than they do with vanilla \LaTeX: instead of
+$\mathit{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;
+some have been redefined---usually to fix the spacing so that it is
+suitable for Z specifications.
+The commands for obtaining additional symbols are listed below.
+Sometimes more than one command may produce a symbol you
+require.  You should use the one that seems to be designed for the
+context you have in mind.  This is because the spacing around (and size of)
+symbols has been chosen for their typical context.
+
+Throughout the lifetime of these macros a number of alternate control
+sequences for any symbol may have existed.  A list of aliases has been
+set up so that old commands may still be used.  It is
+recommended however that you stick to the recommended command
+names for symbols as these names may be supported by other tools.
+Within the table below non-recommended aliases are surrounded by
+brackets, e.g., \verb|(\power)|.
+\begin{multicols}{2}
+\setcounter{secnumdepth}{2}
+\zedindent=0.2\zedindent
+\subsection{Special Z Notation}
+\vspace*{-0.5ex}
+\subsubsection{Numbers}
+\vspace*{-2.5ex}
+\begin{symbols}
+\nat & \verb' \nat' \\
+\natone & \verb' \natone (\nplus)' \\
+\integer & \verb' \integer (\num)' \\
+\real & \verb' \real' \\
+\div~\mod & \verb' \div \mod' \\
+i^n & \verb' i^n i\expon n' \\
+\succ & \verb' \succ' \\
+%\prec & \verb' \prec' \\
+=~\neq & \verb' = \neq' \\
+<~\leq~\leqslant & \verb' < \leq \leqslant' \\
+>~\geq~\geqslant & \verb' > \geq \geqslant' \\
+*\,/\,+ - & \verb' * / + -' \\
+\end{symbols}
+\subsubsection{Logic}
+\vspace*{-2.5ex}
+\begin{symbols}
+\lnot & \verb'\lnot' \\
+\land & \verb'\land (\wedge)' \\
+\lor & \verb'\lor (\vee)' \\
+\all & \verb'\all (\forall)' \\
+\exi & \verb'\exi (\exists)' \\
+\exi_1 & \verb'\exione' \\
+\nexi & \verb'\nexi (\nexists)' \\
+\dot & \verb'@ \dot (\spot)' \\
+%\cond & \verb'\cond' \\
+\imp & \verb'\imp (\implies)' \\
+\iff & \verb'\iff' \\
+\true & \verb'\true' \\
+\false & \verb'\false' \\
+\bool & \verb'\bool' \\
+\end{symbols}
+\subsubsection{Sets}
+\vspace*{-2.5ex}
+\begin{symbols}
+\{~~\cbar~~\} & \verb' \{ \cbar \}' \\
+\emptyset & \verb' \emptyset' \\
+\varemptyset & \verb' \varemptyset' \\
+\mem & \verb' \mem (\in)' \\
+\nmem & \verb' \nem (\nmem \notin)' \\
+\pset & \verb' \pset (\power)' \\
+\fset & \verb' \fset (\finset)' \\
+\psetone~~\fsetone & \verb' \fsetone \psetone' \\
+\uni & \verb' \uni (\union)' \\
+\int & \verb' \int (\inter)' \\
+\psubs & \verb' \psubs (\subset)' \\
+\subs & \verb' \subs (\subseteq)' \\
+\psups & \verb' \psups (\supset)' \\
+\sups & \verb' \sups (\supseteq)' \\
+\prod & \verb' \prod (\cross)' \\
+\min~\max & \verb' \min \max' \\
+\# & \verb' \#' \\
+\duni & \verb' \duni (\dunion)' \\
+\dint & \verb' \dint (\dinter)' \\
+\upto & \verb' \upto' \\
+\end{symbols}
+
+\subsubsection{Relations and Functions}
+\vspace*{-2.5ex}
+\begin{symbols}[0.1]
+\lambda~~~\mu & \verb'\lambda \mu' \\
+\dom & \verb'\dom' \\
+\ran & \verb'\ran' \\
+\dres & \verb'\dres' \\
+\dsub & \verb'\dsub (\ndres)' \\
+\rres & \verb'\rres' \\
+\rsub & \verb'\rsub (\nrres)' \\
+\fovr & \verb'\fovr' \\
+\cmp & \verb'\cmp' \\
+\fcmp & \verb'\fcmp (\comp)' \\
+(\!|~~~|\!) & \verb'\limg \rimg' \\
+\id & \verb'\id' \\
+R\inv & \verb'R^{-1}  R\inv' \\
+R^+ &   \verb'R^+     R\tcl' \\
+R^* &   \verb'R^*     R\rtcl' \\
+R^k &   \verb'R^k     R\iter k' \\
+iter\,0\,R & \verb'iter \, 0 \, R' \\
+\map & \verb'\map' \\
+\rel & \verb'\rel' \\
+\tfun & \verb'\tfun (\fun)' \\
+\tinj & \verb'\tinj (\inj)' \\
+\tsur & \verb'\tsur (\surj)' \\
+\pfun & \verb'\pfun' \\
+\pinj & \verb'\pinj' \\
+\psur & \verb'\psur (\psurj)' \\
+\ffun & \verb'\ffun' \\
+\finj & \verb'\finj' \\
+\bij & \verb'\bij' \\
+\end{symbols}
+\subsubsection{Sequences}
+\vspace*{-2.5ex}
+\begin{symbols}
+\seq & \verb'   \seq' \\
+\seqone & \verb'   \seqone' \\
+\emptyseq & \verb'   \emptyseq' \\
+\lseq~~~\rseq & \verb'   \lseq \rseq' \\
+\head~~\tail & \verb'   \head \tail' \\
+\front~~\last & \verb'   \front \last' \\
+\rev & \verb'   \rev' \\
+\next & \verb'   \next' \\
+\inseq & \verb'   \inseq' \\
+\prefix & \verb'   \prefix' \\
+\suffix & \verb'   \suffix' \\
+\squash & \verb'   \squash' \\
+\cat & \verb'   \cat' \\
+\dcat & \verb'   \dcat' \\
+\dcmp & \verb'   \dcmp' \\
+\dovr & \verb'   \dovr' \\
+\ires & \verb'   \ires' \\
+\sres & \verb'   \sres \filter' \\
+\partitions & \verb'   \partitions' \\
+\disjoint & \verb'   \disjoint' \\
+\end{symbols}
+
+\subsubsection{Schemas}
+\vspace*{-2.5ex}
+\begin{symbols}
+\Delta & \verb'\Delta' \\
+\equiv~~\Xi & \verb'\equiv \Xi' \\
+\pred & \verb'\pred' \\
+\pre & \verb'\pre' \\
+\post & \verb'\post' \\
+\project & \verb'\zproject \project' \\
+\zand & \verb'\zand' \\
+\zor & \verb'\zor' \\
+\zcmp & \verb'\zcmp (\semi)' \\
+\zexi & \verb'\zexi' \\
+\zall & \verb'\zall' \\
+\znot & \verb'\znot' \\
+\zhide & \verb'\zhide (\hide)' \\
+\zfor & \verb'\zfor' \\
+\zimp & \verb'\zimp' \\
+\zeq & \verb'\zeq' \\
+\zovr & \verb'\zovr' \\
+\zpipe & \verb'\zpipe' \\
+\theta & \verb'\theta' \\
+\lsch~~\zbar~~\rsch & \verb'\lsch \zbar \rsch' \\
+.. & \verb'.' \\
+\end{symbols}
+\subsubsection{Bags}
+\vspace*{-2.5ex}
+\begin{symbols}
+\lbag~~~\rbag & \verb'\lbag \rbag' \\
+\bag & \verb'\bag' \\
+\emptybag & \verb'\emptybag' \\
+\items & \verb'\items' \\
+\bagcount & \verb'\bagcount' \\
+\buni & \verb'\buni' \\
+\inbag & \verb'\inbag' \\
+\end{symbols}
+\subsubsection{Definitions and Declarations}
+\vspace*{-2.5ex}
+\begin{symbols}
+::= & \verb'\ddef' \\
+\bbar & \verb'\bbar' \\
+== & \verb'\defs' \also
+\widehat= & \verb'\sdef' \also
+\triangleq & \verb'\varsdef' \\
+,~~\semicolon~~: & \verb', ; :' \\
+\lang~~~\rang & \verb'\lang \rang' \\
+\end{symbols}
+\subsubsection{Miscellaneous}
+\vspace*{-2.5ex}
+\begin{symbols}[0]
+[~~~] & \verb'[ ]' \\
+(~~~) & \verb'( )' \\
+!~~~? & \verb'! ?' \\
+\zlet & \verb'\zlet' \\
+\zwhere & \verb'\zwhere' \\
+\zin & \verb'\zin' \\
+\langle\!|~~~|\!\rangle & \verb'\lblot \rblot' \\
+\intern Bump & \verb'\intern Bump' \\
+\Init & \verb'\Init'\\
+\Exit & \verb'\Exit'
+\end{symbols}
+
+\subsection{Other Special Notation}
+\vspace*{-1ex}
+\subsubsection{Temporal Logic}
+\vspace*{-2.5ex}
+\begin{symbols}
+\always~\uptilnow & \verb'\always \uptilnow' \\
+~&\verb'(\henceforth)'\\
+\atnext~\atlast & \verb'\atnext \atlast' \\
+\eventually~\previously & \verb'\eventually \previously' \\
+\end{symbols}
+\subsubsection{Proofs}
+\vspace*{-2.5ex}
+\begin{symbols}[0.1]
+\TH & \verb'   \TH' \\
+\PR & \verb'   \PR' \\
+\LE & \verb'   \LE' \\
+\ETH~\Qed & \verb'   \qed (\ETH) \Qed' \\
+\QED~\BLACKQED & \verb'   \QED \BLACKQED' \\
+\vdash & \verb'   \shows (\thrm)' \\
+\vDash & \verb'   \vDash' \\
+\refines & \verb'   \refines' \\
+\weakrefine & \verb'   \weakrefine' \\
+\end{symbols}
+\subsubsection{Object Theory}
+\vspace*{-2.5ex}
+\begin{symbols}
+\subclass & \verb'\subclass \isa' \\
+\weaksubclass & \verb'\weaksubclass \islikea' \\
+\supclass & \verb'\supclass' \\
+\weaksupclass & \verb'\weaksupclass' \\
+\hasa & \verb'\hasa \instantiates' \\
+\instancein & \verb'\instancein' \\
+\subtype~~\subtypeeq & \verb'\subtype \subtypeeq' \\
+\suptype~~\suptypeeq & \verb'\suptype \suptypeeq' \\
+\end{symbols}
+\subsubsection{Orders}
+\vspace*{-2.5ex}
+\begin{symbols}
+\mono & \verb'      \mono' \\ % these lines fudged to give more spacing
+\torder & \verb'      \torder' \\
+\porder & \verb'      \porder' \\
+\end{symbols}
+\subsubsection{Word Styles}
+\vspace*{-2.5ex}
+\begin{symbols}[0.4]
+\word{word} & \verb'\word{word}' \\
+\keyword{word} & \verb'\keyword{word}' \\
+\boldword{word} & \verb'\boldword{word}' \\
+\underword{word} & \verb'\underword{word}' \\
+\underkeyword{word} & \verb'\underkeyword{word}' \\
+\underboldword{word} & \verb'\underboldword{word}' \\
+\String{word} & \verb'\String{word}' \\
+\STRING{word} & \verb'\STRING{word}' \\
+a \infix{rel} b & \verb'a \infix{rel} b' \\
+\end{symbols}
+
+\subsection{Special Letter Fonts}
+\vspace*{-1ex}
+\subsubsection{Greek}
+\vspace*{-2.5ex}
+\begin{symbols}
+\alpha & \verb'\alpha' \\
+\beta & \verb'\beta' \\
+\gamma~\Gamma & \verb'\gamma \Gamma' \\
+\delta~\Delta & \verb'\delta \Delta' \\
+\epsilon~\varepsilon & \verb'\epsilon \varepsilon' \\
+\zeta & \verb'\zeta' \\
+\eta & \verb'\eta' \\
+\theta~\vartheta~\Theta & \verb'\theta \vartheta \Theta' \\
+\iota & \verb'\iota' \\
+\kappa~\varkappa & \verb'\kappa \varkappa' \\
+\lambda~\Lambda & \verb'\lambda \Lambda' \\
+\mu & \verb'\mu' \\
+\nu & \verb'\nu' \\
+\xi~\Xi & \verb'\xi \Xi' \\
+\pi~\varpi~\Pi & \verb'\pi \varpi \Pi' \\
+\rho~\varrho & \verb'\rho \varrho' \\
+\sigma~\varsigma~\Sigma & \verb'\sigma \varsigma \Sigma' \\
+\tau & \verb'\tau' \\
+\upsilon~\Upsilon & \verb'\upsilon \Upsilon' \\
+\phi~\varphi~\Phi & \verb'\phi \varphi \Phi' \\
+\chi & \verb'\chi' \\
+\psi~\Psi & \verb'\psi \Psi' \\
+\omega~\Omega & \verb'\omega \Omega' \\
+\end{symbols}
+\subsubsection{Caligraphic}
+\vspace*{-2.5ex}
+\begin{symbols}
+\mathcal{A} & \verb'\mathcal{A}' \\
+\mathcal{B} & \verb'\mathcal{B}' \\
+\mathcal{C} & \verb'\mathcal{C}' \\
+\mathcal{D} & \verb'\mathcal{D}' \\
+\mathcal{E} & \verb'\mathcal{E}' \\
+\mathcal{F} & \verb'\mathcal{F}' \\
+\mathcal{G} & \verb'\mathcal{G}' \\
+\mathcal{H} & \verb'\mathcal{H}' \\
+\mathcal{I} & \verb'\mathcal{I}' \\
+\mathcal{J} & \verb'\mathcal{J}' \\
+\mathcal{K} & \verb'\mathcal{K}' \\
+\mathcal{L} & \verb'\mathcal{L}' \\
+\mathcal{M} & \verb'\mathcal{M}' \\
+\mathcal{N} & \verb'\mathcal{N}' \\
+\mathcal{O} & \verb'\mathcal{O}' \\
+\mathcal{P} & \verb'\mathcal{P}' \\
+\mathcal{Q} & \verb'\mathcal{Q}' \\
+\mathcal{R} & \verb'\mathcal{R}' \\
+\mathcal{S} & \verb'\mathcal{S}' \\
+\mathcal{T} & \verb'\mathcal{T}' \\
+\mathcal{U} & \verb'\mathcal{U}' \\
+\mathcal{V} & \verb'\mathcal{V}' \\
+\mathcal{W} & \verb'\mathcal{W}' \\
+\mathcal{X} & \verb'\mathcal{X}' \\
+\mathcal{Y} & \verb'\mathcal{Y}' \\
+\mathcal{Z} & \verb'\mathcal{Z}' \\
+\end{symbols}
+\subsubsection{BlackBoard Bold}
+\vspace*{-2.5ex}
+\begin{symbols}
+\mathbb A & \verb'\mathbb A' \\
+\mathbb B & \verb'\mathbb B' \\
+\mathbb C & \verb'\mathbb C' \\
+\mathbb D & \verb'\mathbb D' \\
+\mathbb E & \verb'\mathbb E' \\
+\mathbb F & \verb'\mathbb F' \\
+\mathbb G & \verb'\mathbb G' \\
+\mathbb H & \verb'\mathbb H' \\
+\mathbb I & \verb'\mathbb I' \\
+\mathbb J & \verb'\mathbb J' \\
+\mathbb K & \verb'\mathbb K' \\
+\mathbb L & \verb'\mathbb L' \\
+\mathbb M & \verb'\mathbb M' \\
+\mathbb N & \verb'\mathbb N' \\
+\mathbb O & \verb'\mathbb O' \\
+\mathbb P & \verb'\mathbb P' \\
+\mathbb Q & \verb'\mathbb Q' \\
+\mathbb R & \verb'\mathbb R' \\
+\mathbb S & \verb'\mathbb S' \\
+\mathbb T & \verb'\mathbb T' \\
+\mathbb U & \verb'\mathbb U' \\
+\mathbb V & \verb'\mathbb V' \\
+\mathbb W & \verb'\mathbb W' \\
+\mathbb X & \verb'\mathbb X' \\
+\mathbb Y & \verb'\mathbb Y' \\
+\mathbb Z & \verb'\mathbb Z' \\
+\end{symbols}
+\subsubsection{Miscellaneous}
+\vspace*{-2.5ex}
+\begin{symbols}
+\hslash & \verb'\hslash' \\
+\hbar & \verb'\hbar' \\
+\backepsilon & \verb'\backepsilon' \\
+\eth & \verb'\eth' \\
+\beth & \verb'\beth' \\
+\gimel & \verb'\gimel' \\
+\daleth & \verb'\daleth' \\
+\complement & \verb'\complement' \\
+\intercal & \verb'\intercal' \\
+\aleph & \verb'\aleph' \\
+\nabla & \verb'\nabla' \\
+\hbar & \verb'\hbar' \\
+\imath & \verb'\imath' \\
+\jmath & \verb'\jmath' \\
+\ell & \verb'\ell' \\
+\wp & \verb'\wp' \\
+\Re & \verb'\Re' \\
+\Im & \verb'\Im' \\
+\mho & \verb'\mho' \\
+\digamma & \verb'\digamma' \\
+\end{symbols}
+
+\subsection{Shapes}
+\vspace*{-2ex}
+\begin{symbols}
+\Box & \verb'\Box' \\
+\square & \verb'\square' \\
+\blacksquare & \verb'\blacksquare' \\
+\diamond & \verb'\diamond' \\
+\Diamond & \verb'\Diamond' \\
+\lozenge & \verb'\lozenge' \\
+\blacklozenge & \verb'\blacklozenge' \\
+\vartriangleright & \verb'\vartriangleright' \\
+\vartriangleleft & \verb'\vartriangleleft' \\
+\blacktriangledown & \verb'\blacktriangledown' \\
+\blacktriangleright & \verb'\blacktriangleright' \\
+\blacktriangleleft & \verb'\blacktriangleleft' \\
+\vartriangle & \verb'\vartriangle' \\
+\blacktriangle & \verb'\blacktriangle' \\
+\triangledown & \verb'\triangledown' \\
+\triangle & \verb'\triangle' \\
+\triangleleft & \verb'\triangleleft' \\
+\triangleright & \verb'\triangleright' \\
+\bigtriangleup & \verb'\bigtriangleup' \\
+\bigtriangledown & \verb'\bigtriangledown' \\
+\clubsuit & \verb'\clubsuit' \\
+\diamondsuit & \verb'\diamondsuit' \\
+\heartsuit & \verb'\heartsuit' \\
+\spadesuit & \verb'\spadesuit' \\
+\ast & \verb'\ast' \\
+\star & \verb'\star' \\
+\maltese & \verb'\maltese' \\
+\bigstar & \verb'\bigstar' \\
+\bigcirc & \verb'\bigcirc' \\
+\circ & \verb'\circ' \\
+\bullet & \verb'\bullet' \\
+\centerdot & \verb'\centerdot' \\
+\cdot & \verb'\cdot' \\
+\cdots & \verb'\cdots' \\
+\ldots & \verb'\ldots' \\
+\vdots & \verb'\vdots' \\
+\ddots & \verb'\ddots' \\
+\end{symbols}
+\subsubsection{Circled Operations}
+\vspace*{-2.5ex}
+\begin{symbols}
+\circledS & \verb'\circledS' \\
+\circledcirc & \verb'\circledcirc' \\
+\circledast & \verb'\circledast' \\
+\circleddash & \verb'\circleddash' \\
+\circledR & \verb'\circledR' \\
+\copyright & \verb'\copyright' \\
+\fovr & \verb'\fovr' \\
+\ominus & \verb'\ominus' \\
+\otimes & \verb'\otimes' \\
+\oslash & \verb'\oslash' \\
+\odot & \verb'\odot' \\
+\end{symbols}
+
+\subsubsection{Boxed operators}
+\vspace*{-2.5ex}
+\begin{symbols}[0.2]
+\boxdot & \verb'\boxdot' \\
+\boxplus & \verb'\boxplus' \\
+\boxtimes & \verb'\boxtimes' \\
+\boxminus & \verb'\boxminus' \\
+\end{symbols}
+\subsection{Arrow Symbols}
+\vspace*{-1ex}
+\subsubsection{Left Arrows}
+\vspace*{-2.5ex}
+\begin{symbols}[0.7]
+\leftarrow & \verb'\leftarrow   \gets' \\
+\Leftarrow & \verb'\Leftarrow' \\
+\hookleftarrow & \verb'\hookleftarrow' \\
+\leftharpoonup & \verb'\leftharpoonup' \\
+\leftharpoondown & \verb'\leftharpoondown' \\
+\longleftarrow & \verb'\longleftarrow' \\
+\Longleftarrow & \verb'\Longleftarrow' \\
+\twoheadleftarrow & \verb'\twoheadleftarrow' \\
+\leftleftarrows & \verb'\leftleftarrows' \\
+\leftarrowtail & \verb'\leftarrowtail' \\
+\Lleftarrow & \verb'\Lleftarrow' \\
+\nleftarrow & \verb'\nleftarrow' \\
+\nLeftarrow & \verb'\nLeftarrow' \\
+\end{symbols}
+
+\subsubsection{Right Arrows}
+\begin{symbols}[0.7]
+\rightarrow & \verb'\rightarrow \to' \\
+\Rightarrow & \verb'\Rightarrow' \\
+\map & \verb'\map' \\
+\longmapsto & \verb'\longmapsto' \\
+\hookrightarrow & \verb'\hookrightarrow' \\
+\rightharpoonup & \verb'\rightharpoonup' \\
+\rightharpoondown & \verb'\rightharpoondown' \\
+\leadsto & \verb'\leadsto' \\
+\longrightarrow & \verb'\longrightarrow' \\
+\Longrightarrow & \verb'\Longrightarrow' \\
+\twoheadrightarrow & \verb'\twoheadrightarrow' \\
+\rightrightarrows & \verb'\rightrightarrows' \\
+\rightarrowtail & \verb'\rightarrowtail' \\
+\rightsquigarrow & \verb'\rightsquigarrow' \\
+\Rrightarrow & \verb'\Rrightarrow' \\
+\nrightarrow & \verb'\nrightarrow' \\
+\nRightarrow & \verb'\nRightarrow' \\
+\end{symbols}
+
+\subsubsection{Left Right Arrows}
+\begin{symbols}[0.6]
+\leftrightarrow & \verb'\leftrightarrow' \\
+\Leftrightarrow & \verb'\Leftrightarrow' \\
+\rightleftharpoons & \verb'\rightleftharpoons' \\
+\longleftrightarrow & \verb'\longleftrightarrow' \\
+\Longleftrightarrow & \verb'\Longleftrightarrow' \\
+\rightleftharpoons & \verb'\rightleftharpoons' \\
+\leftrightharpoons & \verb'\leftrightharpoons' \\
+\leftrightarrows & \verb'\leftrightarrows' \\
+\rightleftarrows & \verb'\rightleftarrows' \\
+\leftrightsquigarrow & \verb'\leftrightsquigarrow' \\
+\nLeftrightarrow & \verb'\nLeftrightarrow' \\
+\nleftrightarrow & \verb'\nleftrightarrow' \\
+\end{symbols}
+
+\subsubsection{Up Down Arrows}
+\begin{symbols}[1]
+\uparrow & \verb'\uparrow' \\
+\Uparrow & \verb'\Uparrow' \\
+\downarrow & \verb'\downarrow' \\
+\Downarrow & \verb'\Downarrow' \\
+\updownarrow & \verb'\updownarrow' \\
+\Updownarrow & \verb'\Updownarrow' \\
+\upuparrows & \verb'\upuparrows' \\
+\downdownarrows & \verb'\downdownarrows' \\
+\upharpoonright & \verb'\upharpoonright' \\
+\downharpoonright & \verb'\downharpoonright' \\
+\upharpoonleft & \verb'\upharpoonleft' \\
+\downharpoonleft & \verb'\downharpoonleft' \\
+\end{symbols}
+
+\subsubsection{Miscellaneous}
+\begin{symbols}[0.9]
+\nearrow & \verb'\nearrow' \\
+\searrow & \verb'\searrow' \\
+\swarrow & \verb'\swarrow' \\
+\nwarrow & \verb'\nwarrow' \\
+\circlearrowright & \verb'\circlearrowright' \\
+\circlearrowleft & \verb'\circlearrowleft' \\
+\Lsh & \verb'\Lsh' \\
+\Rsh & \verb'\Rsh' \\
+\looparrowleft & \verb'\looparrowleft' \\
+\looparrowright & \verb'\looparrowright' \\
+\curvearrowleft & \verb'\curvearrowleft' \\
+\curvearrowright & \verb'\curvearrowright' \\
+\end{symbols}
+\pagebreak[4]
+
+\subsection{Relations}
+\begin{symbols}[0.8]
+\ll & \verb'\ll' \\
+\gg & \verb'\gg' \\
+\llless & \verb'\lll \llless' \\
+\gggtr & \verb'\ggg \gggtr' \\
+\sqsubset & \verb'\sqsubset' \\
+\sqsupset & \verb'\sqsupset' \\
+\sqsubseteq & \verb'\sqsubseteq' \\
+\sqsupseteq & \verb'\sqsupseteq' \\
+\owns & \verb'\owns' \\
+\vdash & \verb'\vdash' \\
+\Vdash & \verb'\Vdash' \\
+\vDash & \verb'\vDash' \\
+\dashv & \verb'\dashv' \\
+\Vvdash & \verb'\Vvdash' \\
+\models & \verb'\models' \\
+\nvdash & \verb'\nvdash' \\
+\nVdash & \verb'\nVdash' \\
+\nvDash & \verb'\nvDash' \\
+\nVDash & \verb'\nVDash' \\
+\perp & \verb'\perp' \\
+\sim & \verb'\sim' \\
+\simeq & \verb'\simeq' \\
+\eqsim & \verb'\eqsim' \\
+\backsim & \verb'\backsim' \\
+\backsimeq & \verb'\backsimeq' \\
+\thicksim & \verb'\thicksim' \\
+\nsim & \verb'\nsim' \\
+\approx & \verb'\approx' \\
+\napprox & \verb'\napprox' \\
+\thickapprox & \verb'\thickapprox' \\
+\approxeq & \verb'\approxeq' \\
+\asymp & \verb'\asymp' \\
+\cong & \verb'\cong' \\
+\ncong & \verb'\ncong' \\
+\doteq & \verb'\doteq' \\
+\doteqdot & \verb'\Doteq \doteqdot' \\
+\risingdotseq & \verb'\risingdotseq' \\
+\fallingdotseq & \verb'\fallingdotseq' \\
+\lessdot & \verb'\lessdot' \\
+\gtrdot & \verb'\gtrdot' \\
+\eqcirc & \verb'\eqcirc' \\
+\circeq & \verb'\circeq' \\
+\bumpeq & \verb'\bumpeq' \\
+\Bumpeq & \verb'\Bumpeq' \\
+\triangleq & \verb'\triangleq' \\
+\multimap & \verb'\multimap' \\
+\propto & \verb'\propto' \\
+\varpropto & \verb'\varpropto' \\
+\lesssim & \verb'\lesssim' \\
+\gtrsim & \verb'\gtrsim' \\
+\lessapprox & \verb'\lessapprox' \\
+\gtrapprox & \verb'\gtrapprox' \\
+\xprec & \verb'\xprec' \\
+\xsucc & \verb'\xsucc' \\
+\preceq & \verb'\preceq' \\
+\succeq & \verb'\succeq' \\
+\precsim & \verb'\precsim' \\
+\succsim & \verb'\succsim' \\
+\precapprox & \verb'\precapprox' \\
+\succapprox & \verb'\succapprox' \\
+\eqslantless & \verb'\eqslantless' \\
+\eqslantgtr & \verb'\eqslantgtr' \\
+\curlyeqprec & \verb'\curlyeqprec' \\
+\curlyeqsucc & \verb'\curlyeqsucc' \\
+\preccurlyeq & \verb'\preccurlyeq' \\
+\succcurlyeq & \verb'\succcurlyeq' \\
+\leqq & \verb'\leqq' \\
+\geqq & \verb'\geqq' \\
+\leqslant & \verb'\leqslant' \\
+\geqslant & \verb'\geqslant' \\
+\lessgtr & \verb'\lessgtr' \\
+\gtrless & \verb'\gtrless' \\
+\lesseqgtr & \verb'\lesseqgtr' \\
+\Also
+\gtreqless & \verb'\gtreqless' \\
+\Also
+\lesseqqgtr & \verb'\lesseqqgtr' \\
+\Also
+\gtreqqless & \verb'\gtreqqless' \\
+\also
+\lvertneqq & \verb'\lvertneqq' \\
+\gvertneqq & \verb'\gvertneqq' \\
+\nleq & \verb'\nleq' \\
+\ngeq & \verb'\ngeq' \\
+\nless & \verb'\nless' \\
+\ngtr & \verb'\ngtr' \\
+\nprec & \verb'\nprec' \\
+\nsucc & \verb'\nsucc' \\
+\lneqq & \verb'\lneqq' \\
+\gneqq & \verb'\gneqq' \\
+\nleqslant & \verb'\nleqslant' \\
+\ngeqslant & \verb'\ngeqslant' \\
+\lneq & \verb'\lneq' \\
+\gneq & \verb'\gneq' \\
+\npreceq & \verb'\npreceq' \\
+\nsucceq & \verb'\nsucceq' \\
+\precnsim & \verb'\precnsim' \\
+\succnsim & \verb'\succnsim' \\
+\lnsim & \verb'\lnsim' \\
+\gnsim & \verb'\gnsim' \\
+\nleqq & \verb'\nleqq' \\
+\ngeqq & \verb'\ngeqq' \\
+\precneqq & \verb'\precneqq' \\
+\succneqq & \verb'\succneqq' \\
+\precnapprox & \verb'\precnapprox' \\
+\succnapprox & \verb'\succnapprox' \\
+\lnapprox & \verb'\lnapprox' \\
+\gnapprox & \verb'\gnapprox' \\
+\Subset & \verb'\Subset' \\
+\Supset & \verb'\Supset' \\
+\subseteqq & \verb'\subseteqq' \\
+\supseteqq & \verb'\supseteqq' \\
+%\varsubsetneq & \verb'\varsubsetneq' \\
+%\varsupsetneq & \verb'\varsupsetneq' \\
+\nsubseteqq & \verb'\nsubseteqq' \\
+\also
+\nsupseteqq & \verb'\nsupseteqq' \\
+\also
+\subsetneqq & \verb'\subsetneqq' \\
+\also
+\supsetneqq & \verb'\supsetneqq' \\
+%\varsubsetneqq & \verb'\varsubsetneqq' \\
+%\varsupsetneqq & \verb'\varsupsetneqq' \\
+\subsetneq & \verb'\subsetneq' \\
+\supsetneq & \verb'\supsetneq' \\
+\nsubseteq & \verb'\nsubseteq' \\
+\nsupseteq & \verb'\nsupseteq' \\
+\trianglerighteq & \verb'\trianglerighteq' \\
+\trianglelefteq & \verb'\trianglelefteq' \\
+\ntrianglerighteq & \verb'\ntrianglerighteq' \\
+\ntrianglelefteq & \verb'\ntrianglelefteq' \\
+\ntriangleleft & \verb'\ntriangleleft' \\
+\ntriangleright & \verb'\ntriangleright' \\
+\between & \verb'\between' \\
+| & \verb'| \vert \mid' \\
+\| & \verb'\| \Vert \parallel' \\
+\interleave & \verb'\interleave' \\
+\shortmid & \verb'\shortmid' \\
+\shortparallel & \verb'\shortparallel' \\
+\shortinterleave & \verb'\shortinterleave' \\
+\nparallel & \verb'\nparallel' \\
+\nmid & \verb'\nmid' \\
+\nshortmid & \verb'\nshortmid' \\
+\nshortparallel & \verb'\nshortparallel' \\
+\end{symbols}
+
+\subsection{Binary Operations}
+\begin{symbols}[1.4]
+\curlywedge & \verb'\curlywedge' \\
+\curlyvee & \verb'\curlyvee' \\
+\veebar & \verb'\veebar' \\
+\barwedge & \verb'\barwedge' \\
+\doublebarwedge & \verb'\doublebarwedge' \\
+\pm & \verb'\pm' \\
+\mp & \verb'\mp' \\
+\times & \verb'\times' \\
+\ltimes & \verb'\ltimes' \\
+\rtimes & \verb'\rtimes' \\
+\leftthreetimes & \verb'\leftthreetimes' \\
+\rightthreetimes & \verb'\rightthreetimes' \\
+\divideontimes & \verb'\divideontimes' \\
+\divides & \verb'\divides' \\
+\uplus & \verb'\uplus' \\
+\sqcap & \verb'\sqcap' \\
+\sqcup & \verb'\sqcup' \\
+\Cup & \verb'\Cup \doublecup' \\
+\Cap & \verb'\Cap \doublecap' \\
+\backslash & \verb'\backslash' \\
+\setminus & \verb'\setminus' \\
+\smallsetminus & \verb'\smallsetminus' \\
+\wr & \verb'\wr' \\
+\lhd & \verb'\lhd' \\
+\rhd & \verb'\rhd' \\
+\unlhd & \verb'\unlhd' \\
+\unrhd & \verb'\unrhd' \\
+\restriction & \verb'\restriction' \\
+\amalg & \verb'\amalg' \\
+\top & \verb'\top' \\
+\bot & \verb'\bot' \\
+\smallsmile & \verb'\smallsmile' \\
+\smallfrown & \verb'\smallfrown' \\
+\smile & \verb'\smile' \\
+\frown & \verb'\frown' \\
+\pitchfork & \verb'\pitchfork' \\
+\dotplus & \verb'\dotplus' \\
+\Join & \verb'\Join' \\
+\bowtie & \verb'\bowtie' \\
+\end{symbols}
+
+\subsection{Miscellaneous Symbols}
+\begin{symbols}
+\dagger & \verb'\dagger' \\
+\ddagger & \verb'\ddagger' \\
+\sectionsymbol & \verb'\sectionsymbol' \\
+\P & \verb'\P' \\
+\angle & \verb'\angle' \\
+\measuredangle & \verb'\measuredangle' \\
+\sphericalangle & \verb'\sphericalangle' \\
+\prime & \verb'\prime' \\
+\backprime & \verb'\backprime' \\
+\surd & \verb'\surd' \\
+\smallint & \verb'\smallint' \\
+\flat & \verb'\flat' \\
+\natural & \verb'\natural' \\
+\sharp & \verb'\sharp' \\
+\partial & \verb'\partial' \\
+\infty & \verb'\infty' \\
+\yen & \verb'\yen' \\
+\therefore & \verb'\therefore' \\
+\because & \verb'\because' \\
+\checkmark & \verb'\checkmark' \\
+\end{symbols}
+
+\subsection{Variable-sized Symbols}
+These symbols come in two sizes which
+do not vary with the point size of your
+font.  The big size can be obtained
+by preceding the symbol command with
+the command \verb'\displaystyle'.
+\begin{symbols}[1.3]
+\sum \displaystyle \sum & \verb'\sum' \\
+\product \displaystyle \product & \verb'\product' \\
+\coprod \displaystyle \coprod & \verb'\coprod' \\
+\integral \displaystyle \integral & \verb'\integral' \\
+\oint \displaystyle \oint & \verb'\oint' \\
+\bigcap \displaystyle \bigcap & \verb'\bigcap' \\
+\bigcup \displaystyle \bigcup & \verb'\bigcup' \\
+\bigsqcup \displaystyle \bigsqcup & \verb'\bigsqcup' \\
+\bigvee \displaystyle \bigvee & \verb'\bigvee' \\
+\bigwedge \displaystyle \bigwedge & \verb'\bigwedge' \\
+\bigodot \displaystyle \bigodot & \verb'\bigodot' \\
+\bigotimes \displaystyle \bigotimes & \verb'\bigotimes' \\
+\bigoplus \displaystyle \bigoplus & \verb'\bigoplus' \\
+\biguplus \displaystyle \biguplus & \verb'\biguplus' \\
+\end{symbols}
+
+\subsection{Delimiters}
+\vspace*{-1ex}
+These symbols can be made large to surround large formula.
+E.g., $$\left\lfloor\displaystyle\sum_{i=1}^n x^i\right\rfloor$$
+was generated using
+
+\begin{verbatim}
+\left\lfloor...\right\rfloor
+\end{verbatim}
+\vspace*{-2ex}
+\begin{symbols}[0.8]
+(~~~) & \verb'( )' \\
+\{~~~\} & \verb'\{ \}' \\
+\lfloor~~~\rfloor & \verb'\lfloor \rfloor' \\
+\lceil~~~\rceil & \verb'\lceil \rceil' \\
+\langle~~~\rangle & \verb'\langle \rangle' \\
+\ulcorner~~~\urcorner & \verb'\ulcorner \urcorner' \\
+\llcorner~~~\lrcorner & \verb'\llcorner \lrcorner' \\
+\uparrow & \verb'\uparrow' \\
+\downarrow & \verb'\downarrow' \\
+\updownarrow & \verb'\updownarrow' \\
+\Uparrow & \verb'\Uparrow' \\
+\Downarrow & \verb'\Downarrow' \\
+\Updownarrow & \verb'\Updownarrow' \\
+\end{symbols}
+
+\subsection{Math Accents}
+\vspace*{-1ex}
+\begin{symbols}[0.2]
+\hat{a} & \verb'\hat{a}' \\
+\widehat{a} & \verb'\widehat{a}' \\
+\widehat{aa} & \verb'\widehat{aa}' \\
+\widehat{aaa} & \verb'\widehat{aaa}' \\
+\tilde{a} & \verb'\tilde{a}' \\
+\widetilde{a} & \verb'\widetilde{a}' \\
+\widetilde{aa} & \verb'\widetilde{aa}' \\
+\widetilde{aaa} & \verb'\widetilde{aaa}' \\
+\check{a} & \verb'\check{a}' \\
+\breve{a} & \verb'\breve{a}' \\
+\acute{a} & \verb'\acute{a}' \\
+\grave{a} & \verb'\grave{a}' \\
+\bar{a} & \verb'\bar{a}' \\
+\vec{a} & \verb'\vec{a}' \\
+\dotaccent{a} & \verb'\dotaccent{a}' \\
+\ddot{a} & \verb'\ddot{a}' \\
+\end{symbols}
+
+\subsection{Size Commands}
+\vspace*{-1ex}
+\begin{symbols}
+\mu~\zsmall\mu~\zSmall\mu &\verb'\mu \zsmall\mu \zSmall\mu'\\
+\zbig\mu~\zBig\mu~\zBIG\mu &\verb'\zbig\mu \zBig\mu \zBIG\mu'\\
+\end{symbols}
+\end{multicols}
+\end{document}
diff --git a/Master/texmf-dist/doc/latex/objectz/oztest.tex b/Master/texmf-dist/doc/latex/objectz/oztest.tex
new file mode 100644
index 00000000000..fc8ea11c932
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/objectz/oztest.tex
@@ -0,0 +1,206 @@
+\documentclass[11pt]{article}
+\usepackage{oz}
+\def\Out#1{#1 \!\!\rightarrow}
+\def\In#1{\rightarrow\!\! #1}
+\begin{document}
+
+Multi-letter identifiers have been changed to look
+better than they do with vanilla \LaTeX: instead of
+$\mathit{specifications}$, you get $specifications$.
+The letters haven't been spread apart, and the
+ligature $fi$ has been used.
+
+{\tt This is in typewriter font}
+
+
+\begin{schema}{BirthdayBook}
+    known: \pset NAME \\
+    birthday: NAME \pfun DATE
+\ST
+    known = \dom birthday
+\end{schema}
+
+\begin{axdef}
+limit : \nat
+\ST
+limit \leq 65536
+\end{axdef}
+
+\begin{class}{Shape}
+\also
+colour : Colour \\
+\end{class}
+
+\begin{axdef}
+perim : \real
+\ST
+perim > 0
+\end{axdef} 
+
+\begin{axdef}
+ini:State \cross Occ \cross T \fun Bool
+\where
+\forall S:State, i: Occ, t:T \dot ini(S,i,t) \iff \\
+\t1 \theta(\Out{S}, 1,0)\land\\
+\t2 \exi t_{1}:T \dot \theta(\In{S},i,t_{1}) \land
+t_{1}\leq t \land \forall t_{2}:T \dot t_{2} < t \imp \neg \theta(\Out{S},i+1,t_{2}
+)\\
+\t1 \lor \theta(\In{S}, 1,0)\land\\
+\t2 \exi t_{1}:T \dot \theta(\In{S},i,t_{1}) \land
+t_{1}\leq t \land \forall t_{2}:T \dot t_{2} < t \imp \neg
+\theta(\Out{S},i,t_{2})
+\end{axdef}
+
+Let us see if \verb|zbreak| works:
+\typeout{*************************************}
+\typeout{If you get large overfull vboxes now, Oz is not working}
+\typeout{*************************************}
+
+\def \comm{\comment}
+
+\begin{schema}{MakePlan}
+        c? : Company \comm{The company that is making the plan}\\
+        t? : Month \comm{Time period} \\
+        \Xi NFMM \\
+        \Xi AttrOfMarkets \comm{OpenMarkets} \\
+        \Xi Cost \\
+        \Xi AttrOfEconomy \comm{Buying and selling price of quota }\\
+        \Xi AttrOfQuota \\
+        \Xi AttrOfProduction \\
+        \Xi FishingLimitations \\
+        Plans! : Company \fun  Plan \comm{The output is the plan for
+          the company} \\
+\zbreak
+\where
+        \forall v: Vessel; f: Fishery; s: QuotaStock; p: Product; \\
+\t0     l: Landing; t: Month; i: Input @ \\
+\t0     \exists  plan: Plan; Months: \power Month;   \\
+\t0     vs : \power Vessel; fs: \power Fishery ; qs: \power QuotaStock; ls: \power Landing; \\
+\t0     ps : \power Product; \\ 
+\t0     catch: Vessel  \cross Fishery \cross QuotaStock \pfun Tons;  \\
+\t0     MAXnet\_profit:Kronur; fishing\_cost:Kronur; \\
+        \t1  production\_earnings:Kronur; \\
+        \t1  production\_cost:Kronur; quota\_trading\_profit:Kronur;  \\
+\t0     fishing\_days: Vessel \cross Fishery \cross Month \pfun \nat; \\
+\t0     value\_landing: Vessel \fun Kronur;  \\
+\t0     export: Vessel \cross Landing \cross Month \pfun Tons; \\
+        \t1 trade\_in, trade\_out: Landing \cross Month \pfun Tons; \\
+        \t1 prod: Product \cross Month \fun Tons;  \\
+\t0     quota\_rent\_in, quota\_rent\_out, quota\_next\_to, \\
+        \t1 quota\_next\_from, quota\_exch\_to, quota\_exch\_from,\\
+        \t1 quota\_trans\_from, quota\_trans\_to: Vessel \cross QuotaStock \pfun Tons;  \\
+\t0     ExchangeCharge: \num; \comm{charge for changing one species into another} \\
+\t0     quota\_used: Vessel \cross QuotaStock \pfun Tons @  \\
+\zbreak 
+        \t0 Plans! = Plans! \oplus \{c? \mapsto  plan \} \land \\
+        \t0 Months = t? \upto 12  \land \\
+        \t0 i \in Inputs \land \\
+        \t0 vs = Vessels ~ c?  \land  v \in vs \land\\
+        \t0 fs = \{f: Fishery | f \in  \\
+        \t1     (\bigcup \{ v: Vessel | v \in vs @ Fisheries(v) \}) @ f \} \land f \in fs \land \\
+        \t0 qs = \{s: QuotaStock; f: Fishery | \\
+        \t1      f \in fs \land s \in QuotaStocks (f) @ s \} \land s \in qs \land \\
+        \t0 ls = \{s: QuotaStock; f: Fishery | f \in fs \land s \in qs @ \\
+        \t1     Landings~(f,s)  \}  \land l \in ls \land \\
+        \t0 ps = \{p: Product | \\
+        \t1     p \in \bigcup \{ fa: Factory | fa \in Factories~c? @ Products(fa) \} @ p \}  \land  \\
+        \t0 p \in ps \land \\
+\comm{The overall goal is to maximize net profits} \\
+        \t0 MAXnet\_profit = -fishing\_cost+production\_earnings + \\
+        \t1     -production\_cost + quota\_trading\_profit   \land   \comm{A.1}\\
+        \t0 catch ~(v,f,s) = ExpCatch~(v,f,s)* \comm{A.4}\\
+        \t1     \sum_{t: Month | t \in Months} fishing\_days~(v,f,t) \land \\
+\comm{One of the prices LandingPrice or ExportPrice is always zero for any l} \\
+        \t0 (\forall l | l \in ls @ LandingPrice (l) = 0 \lor ExportPrice(l) = 0 \land \\
+        \t1  LandingPrice(l) \neq ExportPrice(l) )  \land \\
+        \t0 value\_landing= \comm{A.3}  \\
+        \t1     \{v: Vessel | v \in vs @ v \mapsto \\
+        \t1     \sum_{ l: Landing | l \in ls}  LandingPrice (l)* ExportPriceConst(l) * \\
+        \t1     \sum_{f: Fishery | f \in fs} \sum_{s: QuotaStock | s \in qs} (SpeciesToLandings~(s,f,l) *(catch~(v,f,s)) \}\land  \\
+        \t0 fishing\_cost = \sum_{v: Vessel | v \in vs} Share (v)*value\_landing(v) + \comm{A.2}\\
+        \t1    \sum_{ f: Fishery | f \in fs} CostFishDay ~ (v, f)  * \\
+        \t1    \sum_{t: Month | t \in Months}  fishing\_days~(v,f,t) \land \\
+\zbreak 
+        \t0 production\_earnings = \comm{A.5}\\
+        \t1     \sum_{l: Landing | l \in ls} \sum_{ t: Month | t \in Months} \\
+        \t3     (ExportPrice~(l,t))*(1-0.002)*t)* \\
+        \t3     \sum_{v: Vessel | v \in vs} export~(v,l,t) \\
+        \t1     -WetfishBuyingPrice(l) * (1-0.002)*t)*trade\_in~(l,t)  \\
+        \t1     +WetfishSellingPrice(l) * (1-0.002)*t)*trade\_out~(l,t)  \\
+        \t1     +\sum_{p: Product | p \in ps} ProductPrice~(p,t) *(1-0.002)*t)* \\
+        \t1      \sum_{t:Month | t \in Months} prod~ (p,t) \land \\
+        \t0 production\_cost = \sum_{i: Input | i \in Inputs} InputCost(i)* \comm{A.6}\\
+        \t1     \sum_{p: Product | p \in ps} InputForProduct(p,i) *    \\
+        \t1     \sum_{ t: Month | t \in Months} prod(p,t) \land \\
+        \t0 ExchangeCharge = 0.005*NextPrice(s) \land  \\
+        \t0 quota\_trading\_profit = -(\sum_{s: QuotaStock | s \in qs } QuotaRentInPrice(s) * \\
+        \t1     \sum_{v: Vessel | v \in vs }  quota\_rent\_in~(v,s)  ) \comm{A.7}\\
+        \t1 + \sum_{s: QuotaStock | s \in qs } QuotaRentOutPrice(s)* \\
+        \t1     \sum_{v: Vessel | v \in vs }  quota\_rent\_out~(v,s)   \\
+        \t1 + \sum_{s: QuotaStock | s \in qs } NextCharge *NextPrice(s)*(1-InterestRate)* \\
+        \t1     \sum_{v: Vessel | v \in vs } quota\_next\_to~(v,s)   \\
+        \t1 + \sum_{s: QuotaStock | s \in qs }  NextPrice(s)*(1-InterestRate) * \\
+        \t1     \sum_{v: Vessel | v \in vs }  quota\_next\_from~(v,s)   \\      
+        \t1 -ExchangeCharge*\sum_{v: Vessel | v \in vs }\sum_{s: QuotaStock | s \in qs } quota\_exch\_to(v,s)   \\
+        \t1 -TransferCharge*\sum_{v: Vessel | v \in vs }\sum_{s: QuotaStock | s \in qs } quota\_trans\_to~(v,s)   \land \\      
+        \t0 \sum_{ f: Fishery | f \in fs } fishing\_days~(v,f,t)  \leq MaxTotFishingDays ~(v,t)  \land \comm{A.9}\\
+\comm{A.6.1 Constraints on fishing time } \\
+        \t0 l \in ExportLandings  \implies \\
+        \t1 \sum_{f: Fishery | f \in fs } \sum_{s: QuotaStock | s \in qs } \comm{A.10} \\
+        \t2     SpeciesToLandings~(s,f,l) * ExpCatch (v,f,s)*fishing\_days(v,f,t)   =  \\
+        \t3             export~(v,l,t) \land \\
+\comm{A.6.2 Processing and selling the catch } \\
+        \t0 l \notin ExportLandings \implies \\
+        \t1 \sum_{v: Vessel | v \in vs } \sum_{f: Fishery | f \in fs } \sum_{s: QuotaStock | s \in qs } \\
+        \t2     SpeciesToLandings~(s,f,l)*ExpCatch~(v,f,s)*fishing\_days~(v,f,t)    \\
+        \t1 = (1 / LandingsToProducts~(p,l)) * prod~(p,t) - trade\_in~(l,t) + trade\_out(l,t) \land \comm{A.11}\\
+\zbreak
+        \t0 \sum_{t: Month | t \in Months } \sum_{p:Product | p \in ps }InputForProduct(p,i)*prod(p,t)   \\
+        \t1 \leq \sum_{i : Input | i \in Inputs } MaxInput~(i,t)  \land \comm{A.13}\\
+        \t0 \sum_{t: Month | t \in Months } \sum_{p: Product | p \in ps } InputForProduct(p,i)*prod~(p,t)   \\
+        \t1   \geq \sum_{i: Input | i \in Inputs } MinInput~(i,t)   \land \comm{A.14}\\
+        \t0 \sum_{t: Month | t \in Months } export~(v,l,t)  \leq MaxExport~(v,l) \land \comm{A.15}\\
+\comm{A.6.3 Constraints because of quota restrictions } \\
+        \t0 quota\_used = \comm{A.17} \\
+        \t1 \{ v:Vessel; s: QuotaStock  |  v \in vs \land  s \in qs @ \\
+        \t2     (v,s) \mapsto \sum_{f: Fishery | f \in fs } (1+QuotaSurcharge~(s,f))* \\
+        \t2 catch~(v,f,s) \}  \land \\
+        \t0 \sum_{v: Vessel | v \in vs } quota\_trans\_to(v,s)- quota\_trans\_from(v,s) =0 \land \comm{A.18} \\
+        \t0 quota\_used(v,s) - quota\_rent\_in(v,s) + quota\_rent\_out(v,s) -   \comm{A.16} \\
+        \t1 quota\_exch\_to(v,s) + quota\_exch\_from(v,s) - \\
+        \t1 quota\_trans\_to(v,s) + quota\_trans\_from(v,s) - \\
+        \t1 quota\_next\_to~(v,s) + quota\_next\_from~(v,s) \leq QuotaLeft~(v,s) \land \\
+        \t0 s = Cod \implies MaxQuotaInto(v,s) = 0 \land \comm{A.19}\\
+        \t0 s \neq Cod \implies MaxQuotaInto(v,s) = 0.05*QuotaAllocated(v,s) \land \\
+        \t1 QuotaValueInto(s)*quota\_exch\_to(v,s) \leq \\
+        \t2     \sum_{s: QuotaStock | s \in qs } MaxQuotaInto~(v,s) \land \\
+        \t0 \sum_{s: QuotaStock | s \in qs } QuotaValueInto (s)*quota\_exch\_to~(v,s) - \comm{A.20}\\
+        \t1 \sum_{s: QuotaStock | s \in qs } QuotaValueFrom(s)* quota\_exch\_from~(v,s)   = 0 \land \\
+        \t0 quota\_next\_from(v,s) \leq (QuotaOver(v,s) / 100)*QuotaAllocated(v,s) \land \comm{A.21}\\
+        \t0 quota\_next\_to~(v,s) \leq (QuotaUnder(v,s) / 100)*QuotaAllocated(v,s) \land \comm{A.22} \\
+\zbreak
+\comm{Bounds} \\
+        \t0 fishing\_days~(v,f,t) \leq MaxFishingDays~(f,t) \land \comm{A.23}\\ 
+        \t0 QuotaAllocated~(v,s) = 0 \implies \\
+        \t1     (quota\_exch\_to~(v,s) = 0 \land  \comm{A.24}\\
+        \t1     quota\_rent\_in~(v,s) = 0 \land \comm{A.25}\\
+        \t1     quota\_trans\_to~(v,s) = 0) \land  \comm{A.26} \\       
+        \t0 QuotaValueInto~s = 0 \implies quota\_exch\_to~(v,s) = 0 \land \comm{A.27}\\
+        \t0 QuotaValueFrom~s = 0 \implies quota\_exch\_from~(v,s) = 0  \comm{A.28}\\
+\zbreak
+        \t0 plan.c = c? \
+        \t0 plan.fishing\_days = fishing\_days \land 
+        \t0 plan.quota\_rent\_out = quota\_rent\_out  \land \\
+        \t0 plan.quota\_rent\_in = quota\_rent\_in \land \\
+        \t0 plan.quota\_trans\_from = quota\_trans\_from \land \\
+        \t0 plan.quota\_trans\_to = quota\_trans\_to \land \\
+        \t0 plan.quota\_next\_from = quota\_next\_from \land \\
+        \t0 plan.quota\_next\_to = quota\_next\_to \land \\
+        \t0 plan.quota\_exch\_from = quota\_exch\_from \land \\
+        \t0 plan.quota\_exch\_to = quota\_exch\_to \land \\
+        \t0 plan.trade\_out = trade\_out \land \\
+        \t0 plan.trade\_in = trade\_in \land \\
+        \t0 plan.prod = prod \land \\
+        \t0 plan.export = export \\
+\end{schema}
+\end{document}