remove vdm package, since license is unstated, author apparently uncontactable, ancient stuff anyway

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

4 files changed, 0 insertions, 2778 deletions

diff --git a/Master/texmf-dist/doc/latex/vdm/vdm.dvi b/Master/texmf-dist/doc/latex/vdm/vdm.dvi
deleted file mode 100644
index 268896fa44e..00000000000
--- a/Master/texmf-dist/doc/latex/vdm/vdm.dvi
+++ /dev/null
diff --git a/Master/texmf-dist/doc/latex/vdm/vdm.tex b/Master/texmf-dist/doc/latex/vdm/vdm.tex
deleted file mode 100644
index ddce8336f38..00000000000
--- a/Master/texmf-dist/doc/latex/vdm/vdm.tex
+++ /dev/null
@@ -1,1562 +0,0 @@
-%%% ====================================================================
-%%%  @LaTeX-file{
-%%%     author          = "Mario Wolczko",
-%%%     version         = "3.02",
-%%%     date            = "14 October 1994",
-%%%     filename        = "vdm.tex",
-%%%     address         = "FORMERLY AT
-%%%                        Dept of Computer Science
-%%%                        The University of Manchester
-%%%                        Oxford Road
-%%%                        Manchester M13 9PL
-%%%                        UK",
-%%%     codetable       = "ISO/ASCII",
-%%%     keywords        = "LaTeX, VDM specification language",
-%%%     supported       = "yes",
-%%%     docstring       = "Documentation for vdm.sty
-%%%                        NOTE
-%%%                        Mario no longer works at Manchester
-%%%                        This is a minimal update to LaTeX2e
-%%%                        By David Carlisle",
-%%%  }
-%%% ====================================================================
-\documentclass{article}
-
-\usepackage{latexsym,vdm,verbatim}
-
-
-
-\title{Typesetting BSI VDM with \LaTeX}
-\author{Mario Wolczko\\
-Dept. of Computer Science\\
-The University\\
-Manchester M13 9PL\\
-U.K.\\
-\texttt{mario@cs.man.ac.uk}, {\tt ...!uknet!man.cs!mario}}
-\date{09 June 1992 \\
-Version 3.01}
-
-\newcommand{\Vdm}{{\tt vdm\/}}
-
-\newenvironment{dangerous}{\par\vspace{5pt}\bgroup\small\noindent}%
-                          {\par\egroup\vspace{5pt}}
-
-\newlength{\righthalf} \setlength{\righthalf}{0.5\textwidth}
-\newlength{\lefthalf}  \setlength{\lefthalf}{0.4\textwidth}
-
-\newenvironment{leftside}{\noindent\hspace{0.1\textwidth}%
-                          \minipage[t]{\lefthalf}\vspace{10pt}%
-                          \noindent\begin{vdm}\leftskip=0pt\VDMindent=0pt}%
-                         {\end{vdm}\endminipage}
-\newenvironment{rightside}{\minipage[t]{\righthalf}\verbatim}%
-                          {\endverbatim\endminipage}
-
-
-\renewcommand{\^}[1]{$\langle${\rm #1\/}$\rangle$}
-
-\newcommand{\mmexp}{\^{math-mode-expression}}
-\newcommand{\cs}[1]{\leavevmode\hbox{\tt \string#1}}
-
-\setlength{\VDMindent}{3\parindent}
-
-\setlength{\preOperationSkip}{0pt}
-\setlength{\preFunctionSkip}{0pt}
-\setlength{\preTypeSkip}{0pt}
-\setlength{\preCompositeSkip}{0pt}
-\setlength{\preRecordSkip}{0pt}
-\setlength{\preFormulaSkip}{0pt}
-
-\begin{document}
-
-\maketitle
-
-\tableofcontents
-
-\section{Overview}
-
-This document describes a style option, \Vdm, for use with
-\LaTeX.  The purpose of \Vdm\ is to make the typesetting of VDM
-specifications easy.  Other goals are:
-\begin{itemize}
-\item   To enable users of \Vdm\ to communicate their specifications
-        to others, possibly in a variety of concrete syntaxes, without
-        having to change their source files
-\item   To enable a user of \Vdm\ to concentrate on his%
-        \footnote{Read `his/her' for every occurence of `his'.}
-        specifications, and ignore the detailed layout as much as
-        possible.  A side effect of this is that the effort required
-        to improve layout is concentrated in one place, within the
-        \Vdm\ macros.
-\end{itemize}
-(This version of the \Vdm\ style option uses the {\sc bsi} concrete
-syntax.  Any document prepared using earlier versions is still
-accepted, but the way it is typeset will match more closely the {\sc
-bsi} standard concrete syntax.  There are also a few additional
-commands (summarised at the end).  Note that this is {\em not\/} a
-complete style file for all of {\sc bsi vdm}.)
-
-But enough evangelising.  Let's get to the the real meat.  This
-document is broken up into the following sections:
-\begin{itemize}
-\item   General points about using \Vdm
-\item   Typesetting formulas
-\item   How to typeset data types
-\item   How to typeset functions
-\item   How to typeset operations
-\item   How to typeset proofs
-\item   How to tailor/extend the system for your own
-        application.
-\end{itemize}
-You should definitely read the first two sections---then you'll know
-roughly what you're in for, and whether you want to continue.  The
-remaining sections can be read as and when you need them.
-
-\begin{dangerous}
-In keeping with the best traditions of \TeX\ documentation, paragraphs
-that contain material that is not essential for novices, but vital if
-you want to parameterise or extend the system, are in smaller type,
-like this one.
-\end{dangerous}
-
-Just to give a preliminary example, here is some output from \Vdm, and
-the corresponding input:
-
-\begin{vdm}
-\begin{fn}{dec}{ptrs,om} \\
-\signature{
-         \setof{Oop} \x \mapof{Oop}{Object} \to \mapof{Oop}{Object}
-}
-\If ptrs = \emptyset
-\Then om
-\Else   \Let gone = \set{p \in ptrs | RC(om(p)) = 1} \In
-        \Let om' = gone \dsub om \In
-        \Let om'' = om' \owr
-                \map{p \mapsto \chg{om'(p)}{RC}{RC\minus 1}\R
-                        | p \in ptrs \diff gone} \In
-        dec(\Union\set{\elems{BODY(om(p))} | p \in gone}, om'')
-\Fi
-\end{fn}
-
-\begin{op}[DESTROYPTR]\label{op-ex}
-\args{ Obj, Ptr : Oop }
-\ext{ \Wr OM : \mapof{Oop}{Basic_Object} }
-\pre{ ptr \in  \elems{BODY(om(obj))} }
-\post{ om = ~{om} \owr \map{ obj \mapsto
-                \chg{om(obj)}{BODY}{BODY \diff \set{ptr}}}}
-\end{op}
-\end{vdm}
-
-% this is verbatim input
-\begin{verbatim}
-\begin{vdm}
-\begin{fn}{dec}{ptrs,om} \\
-\signature{
-      \setof{Oop} \x \mapof{Oop}{Object} \to \mapof{Oop}{Object}
-}
-\If ptrs = \emptyset
-\Then om
-\Else   \Let gone = \set{p \in ptrs | RC(om(p)) = 1} \In
-        \Let om' = gone \dsub om \In
-        \Let om'' = om' \owr
-                \map{p \mapsto \chg{om'(p)}{RC}{RC\minus 1}
-                        | p \in ptrs \diff gone} \In
-        dec(\Union\set{\elems{BODY(om(p))} | p \in gone}, om'')
-\Fi
-\end{fn}
-
-\begin{op}[DESTROYPTR]
-\args{ Obj, Ptr : Oop }
-\ext{ \Wr OM : \mapof{Oop}{Basic_Object} }
-\pre{ ptr \in  \elems{BODY(om(obj))} }
-\post{ om = ~{om} \owr \map{ obj \mapsto
-                \chg{om(obj)}{BODY}{BODY \diff \set{ptr}}}}
-\end{op}
-\end{vdm}
-
-\end{verbatim}
-
-
-
-\section{Using \Vdm---General Points}
-
-To get at \Vdm, include {\tt vdm\/} as a document style option, e.g.:
-\begin{verbatim}
-        \documentstyle[12pt,vdm]{report}
-\end{verbatim}
-\begin{dangerous}
-To the best of my knowledge, the use of \Vdm\ does not conflict with
-any of the other document styles, except when something has been
-redefined.   An attempt will be made to document all such redefinitions.
-\end{dangerous}
-Once \Vdm\ has been included, you can then use the {\tt vdm\/}
-environment.  For example,
-\begin{verbatim}
-         \begin{vdm}
-            ....
-         \end{vdm}
-\end{verbatim}
-All specification material should be placed within the {\tt vdm\/}
-environment.  The use of \Vdm\ only affects text within the {\tt vdm\/}
-environment, except for the following global changes (which are only
-relevant when in math or display math mode):
-
-
-\begin{enumerate}
-\item   The mathcodes of a\dots z and A\dots Z have been changed.  In
-        plain English, this means that when you type letters in math
-        mode the inter-letter spacing may be different than it would be
-        had you not included \Vdm\ as an option.\footnote{This is not
-        the case if you are using PS\LaTeX, as that does not
-        distinguish text italic from math italic.}  This is because
-        \LaTeX\ math mode is usually tuned for single letter
-        identifiers, as used by mathematicians for millenia.  However,
-        you and I both know that most meaningful identifiers have more
-        than one letter in them, so \Vdm\ provides better spacing for
-        them.  As an example, if you type \verb;$identifier$;, \LaTeX\
-        would normally print {\defaultMathcodes$identifier$}, whereas
-        the use of \Vdm\ will yield $identifier$.
-        \begin{dangerous}If you really want to use the
-        `normal' inter-letter spacing, say \cs\defaultMathcodes.
-        \end{dangerous}
-\item   Underscore gives you an underscore, and not a subscript.  If
-        you want a subscript use \verb;@;, e.g.,~$x@0$ is typed
-        \verb;x@0;, or use \TeX's \cs\sb\ macro.  An \verb;@; is still an
-        @ when not in math mode.  Occasionally you may find that an @
-        in math mode {\em doesn't\/} give you a subscript
-        (particularly when used with moving arguments).  Should
-        this happen, you are advised to use \TeX's \cs\sb\ macro,
-        e.g.,~\verb;$x\sb{0}$;.
-        \begin{dangerous}
-        If you don't use
-        underscores much, and you want to use \verb;_; for subscripts,
-        you can say \cs\underscoreon\ (and \cs\underscoreoff\ to
-        make it revert to its usual meaning in \Vdm).
-        \end{dangerous}
-\item   \verb;-; typesets a hyphen, and not a minus sign.  VDM specifications
-        usually contain a lot more
-        \begin{vdm}$long-identifiers$\end{vdm}\
-        than subtractions, so
-        on the whole this alteration should save effort.
-        If you really want
-        to do a single subtraction sign, use \cs\minus.
-        If you find the default is inappropriate, you can revert to
-        the original behaviour using \cs\mathminus; \cs\textminus\ is
-        the inverse.  Example: \verb;a-b \ne\mathminus a-b; gives
-        \begin{vdm}$a-b \ne\mathminus a-b$\end{vdm}.
-\item   \verb;|; gives you a \begin{vdm}$|$\end{vdm}, and not a $\vert$.
-        Do you see the difference?  No?  The former goes between things,
-        e.g., \begin{vdm}$\set{x|p(x)}$\end{vdm}, while the latter is
-        a delimiter, e.g.,~$\vert x\vert$.
-        In VDM, most people use the former more than the latter, so again this
-        seems reasonable.
-        If you really want a $\vert$ (the second kind),
-        say \cs\vert.
-\item   In \TeX\ and \LaTeX\ \verb;~; has always been a tie (a space
-        between words at which the line is never broken).  Well
-        in \Vdm\ it isn't.  \verb;~x; will give you a
-        \begin{vdm}$~x$\end{vdm}.  For long identifiers, such as
-        \begin{vdm}$~{long}$\end{vdm}, say
-        \verb;~{long};.
-        {\em Note that this only applies in math
-        mode; elsewhere a \verb;~; is still a tie.}
-\item   In math mode, the double quote character \verb;''; is actually
-        a macro.  Placing text between pairs of double quotes causes
-        that text to be set in the normal text font.  For example,
-        \verb;$x="a variable"$; gives you $x="a variable"$.
-        \begin{dangerous}
-        \indent If you want to change the font used for text placed between
-        quotes, redefine the command \cs\mathTextFont.  By default
-        it is defined to be \cs\rm\ (\cs\mathrm\ for the New Font
-        Selection Scheme).
-        \end{dangerous}
-\item   The following macros have been altered in a non-trivial way:
-        \cs\forall, \cs\exists\ (see later).
-\end{enumerate}
-
-\begin{dangerous}
-When you typeset some VDM within the {\tt vdm\/} environment, by
-default it is set in from the left margin by an amount equal to
-\cs\parindent, the indentation at the beginning of each paragraph.
-If you want to change this, change the value of \cs\VDMindent, e.g.:
-\begin{verbatim}
-        \setlength{\VDMindent}{0cm}
-\end{verbatim}
-will make your specs come out flush left.  This document has been
-typeset with \cs\VDMindent\ equal to $3\times \cs\parindent$.
-
-Similarly, the right hand margin is controlled by a parameter called
-\cs\VDMrindent.  By default it is also set to \cs\parindent.
-\end{dangerous}
-
-\begin{dangerous}
-You can have a particular line spacing in force within the
-{\tt vdm} environment.
-The spacing within a {\tt vdm} environment is dictated by the
-\cs\VDMbaselineskip\ command.  Note that this is {\em not\/} a
-length, but a command.  By default it expands to \cs\baselineskip\
-so that the line spacing is that of the surrounding text, whatever
-size that may be.  To make it smaller, you may want to say
-\begin{verbatim}
-    \renewcommand{\VDMbaselineskip}{0.8\baselineskip}
-\end{verbatim}
-for example.
-\end{dangerous}
-
-
-\section{Typesetting formulas}
-
-Most of the text you enter within {\tt vdm\/} environments will be in
-\TeX's math mode, but VDM does its best to conceal this fact from you,
-so that you should rarely, if ever, have to type a dollar sign.
-However, several new features have been provided for the typesetting
-of logical formulas.  Firstly, operators with sensible names have been
-provided: use \cs\Iff, \cs\Implies, \cs\Or, \cs\And\
-and \cs\Not\ for the operators~\begin{vdm}%
-$\Leftrightarrow,\Rightarrow,\Or,\And$ and $\Not$\end{vdm}.
-(To retain compatibility with a previous version, \cs\iff,
-\cs\implies, \cs\and\ and \cs\neg\ are still provided, but
-\cs\or\ is not.)
-
-A major change has come in the area of quantified expressions.  In
-VDM, they
-have very well-defined forms, so the \LaTeX\ sequences \cs\forall\
-and \cs\exists\ have been re-defined to take arguments.  For
-example, to get
-\begin{vdm}
-\begin{formula}
-\exists{x \in S}{p(x)}
-\end{formula}
-\end{vdm}
-\noindent type
-\begin{verbatim}
-        \exists{x \in S}{p(x)}
-\end{verbatim}
-Note the separating dot that was put in auto\-matically.  If you want
-one of these dots by itself, you can have one by saying
-\cs\suchthat.
-
-In addition, two new quantifiers, \cs\unique\ and \cs\nexists, have
-been added:
-
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-\begin{formula}
-\unique{x \in S}{p(x)}
-\end{formula}
-\begin{formula}
-\nexists{x \in S}{p(x)}
-\end{formula}
-\end{leftside}\begin{rightside}
-\unique{x \in S}{p(x)}
-\nexists{x \in S}{p(x)}
-\end{rightside}
-\end{minipage}
-
-Additionally, to complement \cs\unique, there is \cs\uniqueval.  This
-is the so-called ``iota-function'' that returns the unique value, if
-there is one:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-\begin{formula}
-\uniqueval{x \in S}{p(x)}
-\end{formula}
-\end{leftside}\begin{rightside}
-\uniqueval{x \in S}{p(x)}
-\end{rightside}
-\end{minipage}
-
-
-\begin{dangerous}
-If you want to use the old versions of \cs\forall\ and
-\cs\exists\ they are available under the pseudonyms of
-\cs\Forall\ and \cs\Exists.
-\end{dangerous}
-
-If you find that the body of the quantified expression is too long to
-fit comfortably on a line, there are *-forms of the above commands
-that place the body of the quantified expression on a new line,
-slightly indented.  For example,
-
-\begin{vdm}
-\begin{formula}
-\exists*{x \in S}{
-        p(x) \And q(x) \Or \Not p(x) \Implies r(x) \And S(x)}
-\end{formula}
-\end{vdm}
-
-\noindent can be obtained with
-\begin{verbatim}
-      \exists*{x \in S}{p(x) \And q(x) \Or \Not p(x)
-                        \Implies r(x) \And S(x)}
-\end{verbatim}
-
-If you need ``Strachey'' brackets, e.g., $M\term{e}$, place the
-material to appear within the brackets within \verb;\term{ ... };,
-thus: \verb;$M\term{e}$;.
-
-A special control sequence, \cs\const, is available for constants.
-To get, for example, $\const{Yes}|\const{No}$, type
-\verb;\const{Yes}|\const{No};.
-\begin{dangerous}
-If you don't like the font that constants are set in, you can change
-them by redefining the command \cs\constantFont.  By
-default it expands to \cs\sc.
-\end{dangerous}
-
-\subsection{The {\tt formula} Environment}
-
-Occasionally you may want a formula on its own, between paragraphs of
-text, say.  Normally, the provided environments and commands suffice,
-but sometimes they don't.  If you need an odd equation to stand on its
-own, use the {\tt formula} environment:
-\begin{verbatim}
-       \begin{formula}
-       x = 10
-       \Or  \forall{i \in \Nat}{i \ne 10 \Implies i \ne x}
-       \end{formula}
-\end{verbatim}
-\sloppy
-The {\tt formula} environment is similar to displayed math mode,
-except: formulas are indented by \cs\VDMindent, not
-\cs\mathindent, and line breaks can be made using \cs\\.
-Also, within the {\tt formula} environment everything appears flush
-left, as opposed to being centred.
-
-\subsection{Constructions}
-
-A particularly nice feature of \Vdm\ is that you can typeset multi-line
-constructions such as those in the earlier example without having to
-worry about, say, lining up ``thens'' and ``elses'' with ``ifs''.
-In the following definitions, whenever you see the term \mmexp, you
-should type an expression as if in math mode, but you needn't put
-dollar signs in.  All of the constructions described below can be used
-where a \mmexp\ is required.  Each construction is shown by example;
-the output on the left results from the input on the right.
-Also note that each macro name begins with an upper-case letter.
-\TeX\ and \LaTeX\ frequently use the lower-case variants for
-completely unrelated things.  Naturally, chaos will ensue if you mix
-the names up.
-
-Typesetting an \kw{if} is done using \cs\If\ \mmexp \cs\Then\ \mmexp
-\cs\Else\ \mmexp \cs\Fi.
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-  \begin{formula}
-    \If x\in S
-    \Then S \diff x
-    \Else \emptyset
-    \Fi
-  \end{formula}
-\end{leftside}%
-\begin{rightside}
-\If x\in S
-\Then S \diff x
-\Else \emptyset
-\Fi
-\end{verbatim}
-\end{rightside}
-\end{minipage}
-
-If you nest \cs\If{}s then you must enclose inner \cs\If{}s within
-braces:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-  \begin{formula}
-        \If \ldots
-        \Then{
-                \If \ldots
-                \Then \ldots
-                \Else \ldots
-                \Fi
-        }\Else
-        \Fi
-  \end{formula}
-\end{leftside}\begin{rightside}
-\If ...
-\Then{
-        \If ...
-        \Then ...
-        \Else ...
-        \Fi
-}\Else
-\Fi
-\end{rightside}
-\end{minipage}
-
-You are advised to place the extra braces exactly as above; don't let
-extraneous spaces intervene between the keywords and the braces.
-
-The \cs\If\ macro always starts a new line for the \kw{then} and
-\kw{else} parts.  If you want \TeX\ to try to choose line breaks, use
-\cs\SIf\ instead:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-  \begin{formula}
-    \SIf a=b
-    \Then c=d+e
-    \Else p=q+r+s+t+u
-    \Fi
-  \end{formula}
-\end{leftside}%
-\begin{rightside}
-\SIf a=b
-\Then c=d+e
-\Else p=q+r+s+t+u
-\Fi
-\end{rightside}
-\end{minipage}
-
-\mbox{\kw{let}\dots\kw{in}} constructions are done in a similar way:
-\cs\Let{} \mmexp{} \cs\In{} \mmexp, and \cs\SLet{} \mmexp{}
-\cs\In{} \mmexp.
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-  \begin{formula}
-    \Let x=f(y,z) \In
-    g(x)+h(x)
-  \end{formula}
-\end{leftside}%
-\begin{rightside}
-\Let x=f(y,z) \In
-g(x)+h(x)
-\end{rightside}
-\end{minipage}
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-  \begin{formula}
-    \SLet x=f(y,z) \In{x^2}
-  \end{formula}
-\end{leftside}%
-\begin{rightside}
-\SLet x=f(y,z) \In{x^2}
-\end{rightside}
-\end{minipage}
-
-Notice that \cs\SLet\ takes a second argument, which is part of the
-same `paragraph', where \cs\Let\ does not.
-
-The typesetting of a \kw{cases} clause is more complicated.  It takes
-the form:
-\begin{verse}
-\verb;\Cases{; \mmexp \verb;}; \\
-from-\mmexp \verb;&; to-\mmexp \cs\\ \\
-from-\mmexp \verb;&; to-\mmexp \cs\\ \\
-\dots \\
-\verb;\Otherwise{; \mmexp \verb;}; \\
-\verb;\Endcases;
-\end{verse}
-
-The \cs\Otherwise\ field is optional.  This construction follows a
-general pattern that is common in \Vdm\ input:  lists of things are
-separated by \cs\\s, and subfields are separated by \verb;&;s or
-\verb;:;s.
-\begin{dangerous}
-In reality, there is another, optional argument, after the
-\cs\Endcases.  If you were to try typesetting something like
-\begin{verbatim}
-        (... var = \Cases ...
-                   \Endcases)
-\end{verbatim}
-you'd find the closing right parenthesis in an unexpected place (on
-the same line as the $=$, in fact).  To get text to the right of the
-\cs\Endcases\ you can place an optional argument within brackets
-after it:
-\begin{verbatim}
-        (... var = \Cases ...
-                   \Endcases[)]
-\end{verbatim}
-Admittedly, this looks a little strange, but it does work.
-\end{dangerous}
-
-Here is an example of \cs\Cases\ in action:
-
-\begin{formula}
-  \Cases{ select(x) }
-  \nil            & \emptyset \\
-  mk-Lst(hd,tl)  & \set{hd} \union \elems{tl}
-  \Otherwise{ x }
-  \Endcases
-\end{formula}
-
-\begin{verbatim}
-     \Cases{ select(x) }
-     \nil            & \emptyset \\
-     mk-Lst(hd,tl)  & \set{hd} \union \elems{tl}
-     \Otherwise{ x }
-     \Endcases
-\end{verbatim}
-
-Note the \cs\\ is a {\em separator\/} and not a {\em
-terminator\/}---you don't need one after the last item.  Also, the
-\cs\Otherwise\ can appear anywhere between the \verb;\Cases{}; and the
-\cs\Endcases, but it will always be typeset last.
-\begin{dangerous}
-Some people prefer the selectors to appear lined up on the left, some
-on the right.  If you want them to appear on the left, say
-\cs\leftCases; if you want them on the right, say
-\cs\rightCases.  The scope of the \cs\leftCases\ and
-\cs\rightCases\ commands is the current group.  By default, you
-get \cs\rightCases.
-\end{dangerous}
-
-\subsubsection{The {\tt formbox} Environment}
-
-Occasionally you might find that you want to put a line break in a
-place that can't handle \cs\\.  For example, if you have a \cs\Cases\
-command and the rhs of a particular case is too big, you can't use
-\cs\\ to break the line directly, as it will be interpreted as the
-separator between cases.  Then you must the {\tt formbox} environment.
-It is similar to the {\tt formula} environment in that you can put all
-sorts of things in it, but it can be used within other constructions,
-unlike the {\tt formula} environment, which can only be used at the
-outermost level.
-
-This example should convey the general idea:
-\begin{verbatim}
-        \Cases{ f(x) }
-        mk-Very_long_constructor(foo,bar) &
-            {\begin{formbox}
-            long_predicate_with(foo) \\
-              \And long_predicate_with(bar)
-            \end{formbox}}
-        ...
-\end{verbatim}
-\begin{vdm}
-\begin{formula}
-        \Cases{ f(x) }
-        mk-Very_long_constructor(foo,bar) &
-            {\begin{formbox}
-            long_predicate_with(foo) \\
-              \And long_predicate_with(bar)
-            \end{formbox}}\\
-        \ldots
-        \Endcases
-\end{formula}
-\end{vdm}
-Note the extras braces around the {\tt formbox}; these are required to
-``hide'' the \cs\\ from the \cs\Cases.
-
-\subsection{Other General Points about Formulas}
-
-\cs\\ will%
-\footnote{For `will' read `should'.}
-{\em always\/}
-start a new line.  Sometimes this is done in addition to some other
-function (as in the \cs\Cases\ macro, where it delimits a
-particular case), but you should be able to use \cs\\ almost
-anywhere to force a line break.  Indeed, sooner or later you'll want
-to typeset a long formula and \TeX\ will not be able to break the line
-sensibly, or will choose an unpleasant break.  In this case you'll
-have to use \cs\\.
-
-Frequently you need to indent things within multi-line formulas.  To
-help you do this, a command is provided which breaks a line, and
-indents the next line by an amount which you can supply (in units of
-{\tt ems}).  The \cs\T\ command takes a single argument that controls
-how much the next line will be indented:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-\begin{formula}
-a \And b \T2
-\Implies b \And a \T1
-\Or d \And e
-\end{formula}
-\end{leftside}\begin{rightside}
-a \And b \T2
-\Implies b \And a \T1
-\Or d \And e
-\end{rightside}
-\end{minipage}
-
-Along similar lines is the \cs\R\ command.  This does a line break,
-like \cs\\, but then pushes the formula on the next line as far to the
-right as it can:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-\begin{formula}
-(a \And b \Implies b \And a) \R
-\Or d \And e
-\end{formula}
-\end{leftside}\begin{rightside}
-(a \And b \Implies b \And a) \R
-\Or d \And e
-\end{rightside}
-\end{minipage}
-
-Beware: it may end up pushing it further to the right than you
-expected!  This is {\sc A Bug}, and {\sc Will Not Be Fixed}, so you'll
-have to work around it.
-
-The \cs\If, \cs\Let, etc., constructions are all unusual in
-that it's impossible to typeset something sensibly to the right of
-them.  For example, if you try
-\begin{verbatim}
-        \exists{x \in S}{
-           \If x=0 \Then S=Q \Else S=P \Fi}
-        \Or S=\emptyset
-\end{verbatim}
-then you'll get
-
-\begin{vdm}
-  \begin{formula}
-    \exists{x \in S}{\If x=0 \Then S=Q \Else S=P \Fi} \Or S=\emptyset
-  \end{formula}
-\end{vdm}
-
-\noindent which is unlikely to be what you wanted.
-
-You should also remember that where \Vdm\ wants a \mmexp, \TeX\ will
-be placed in math mode.  This is usually the right thing to do, but
-occasionally you might want a natural language comment to appear
-there.
-In this case you'll have to insert an \cs\mbox\ or a \cs\parbox\
-depending on whether your comment might span one or more lines:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-  \begin{formula}
-    \If \mbox{the condition is true}
-    \Then \mbox{do the true part}
-    \Else "do the false part"
-    \Fi
-  \end{formula}
-\end{leftside}\begin{rightside}
-\If \mbox{the condition is true}
-\Then \mbox{do the true part}
-\Else "do the false part"
-\Fi
-\end{rightside}
-\end{minipage}
-The else-part illustrates how quotes can be used an an abbreviation
-for \verb;\mbox{...}; within math mode.
-
-Finally, all the constructions above will not break at a page
-boundary.  This means that you're in big trouble if you want to
-typeset a three-page \cs\Cases.  The only statement I can make to
-mitigate this is: you shouldn't have expressions that complicated in
-the first place---who do you expect to read them?  Remember: ``truth
-is beauty'', so if your formulas are not beautiful, then chances are
-they're not true either.
-
-
-
-
-
-\section{Typesetting data types}
-
-The following table lists the primitive types and values available:
-
-\begin{center}
-\begin{tabular}{|l|l|l|}
-\hline
-$\set{0,1,\dots}$       & $\Nat$        & \cs\Nat       \\
-$\set{1,2,\dots}$       & $\Natone$     & \cs\Natone,\cs\Nati   \\
-$\set{\dots,\minus1,0,1,\dots}$& $\Int$ & \cs\Int       \\
-Rationals               & $\Rat$        & \cs\Rat       \\
-Real numbers            & $\Real$       & \cs\Real      \\
-$\set{\true,\false}$    & $\Bool$       & \cs\Bool      \\
-Truth                   & $\true$       & \cs\true,\cs\True \\
-Falsehood               & $\false$      & \cs\false,\cs\False\\
-Nil                     & $\nil$        & \cs\nil       \\
-\hline
-\end{tabular}
-\end{center}
-
-If you need a new keyword, you can create one easily.  For example, if
-your favourite brand of logic has ``maybe'' as a value, you can say
-\begin{verbatim}
-        \makeNewKeyword{\maybe}{maybe}
-\end{verbatim}
-and henceforth \cs\maybe\ is a valid control sequence that produces
-the text \kw{maybe}.  The text of the second argument to
-\cs\makeNewKeyword\ can be anything; it doesn't have to match your
-control sequence name.
-\begin{dangerous}
-If you don't like the font that keywords are set in, you can change
-it by redefining the command \cs\keywordFontBeginSequence.  By
-default it expands to \cs\sf.
-\end{dangerous}
-
-The following type-related commands are provided:
-
-\begin{center}
-\begin{tabular}{|l|l|l|}
-\hline
-Output          & Input                 & \\
-\hline
-$\setof{x}$     & \verb;\setof{x};      & set type constructor \\
-$\set{a,b,c}$   & \verb;\set{a,b,c};    & set enumeration \\
-$\emptyset$     & \cs\emptyset          & the empty set \\
-$\seqof{x}$     & \verb;\seqof{x};      & seq. type constructor\\
-$\seq{a,b,a,c}$ & \verb;\seq{a,b,a,c};  & seq. enumeration\\
-$\emptyseq$     & \cs\emptyseq  & the empty sequence \\
-$\mapof{x}{y}$  & \verb;\mapof{x}{y};   & map type constructor \\
-$\mapinto{x}{y}$& \verb;\mapinto{x}{y}; & one-one map type \\
-$\map{p\mapsto x}$
-                & \verb;\map{p\mapsto x}; & map enumeration\\
-$\emptymap$     & \cs\emptymap  & the empty map \\
-\hline
-\end{tabular}
-\end{center}
-
-\noindent Here are the relevant operators:
-
-\begin{center}\small
-\begin{tabular}{llllll}
-$\in$           & \cs\in        &
-        $\owr$  & \cs\owr       &
-                $\sconc$        & \cs\sconc     \\
-$\notin$        & \cs\notin     &
-        $\dres$ & \cs\dres      &
-                $\len{l}$       & \verb;\len{l};\\
-$\subset$       & \cs\subset&
-        $\rres$ & \cs\rres      &
-                $\hd{l}$        & \verb;\hd{l}; \\
-$\subseteq$     & \cs\subseteq&
-        $\dsub$ & \cs\dsub      &
-                $\tl{l}$        & \verb;\tl{l}; \\
-$\inter$        & \cs\inter,\cs\intersection;&
-        $\rsub$ & \cs\rsub      &
-                $\elems{l}$     & \verb;\elems{l};\\
-$\Inter$        & \cs\Inter,\cs\Intersection;&
-        $\dom{m}$&\verb;\dom{m};&
-                $\inds{l}$      & \verb;\inds{l};\\
-$\union$        & \cs\union     &
-        $\rng{m}$&\verb;\rng{m};&
-                $\Conc{l}$      & \verb;\Conc{l};\\
-$\Union$        & \cs\Union     &
-        $\Min{s}$& \verb;\Min{s};&
-                $\cons{h,t}$    & \verb;\cons{h,t};\\
-$\diff$         & \cs\diff,\cs\difference;&
-        $\Max{s}$& \verb;\Max{s};&
-                                &       \\
-$\card{s}$      & \verb;\card{s};&
-                &               &
-                                &
-\end{tabular}
-\end{center}
-
-\begin{dangerous}
-If you invent a new monadic keyword operator (like \dom{}, etc.),
-then you can have \Vdm\ define for you a control sequence which
-switches font, and puts the right spacing in.  For example,
-\begin{verbatim}
-        \newMonadicOperator{\inv}{inv}
-\end{verbatim}
-will define the \cs\inv\ control sequence to print
-{\keywordFontBeginSequence inv\/}.  Henceforth you can say, e.g.,
-\verb;\inv{Foo};.  All such sequences take one argument (they are
-monadic, after all).
-\end{dangerous}
-
-You can define a new type using
-\verb;\type{;type-name\verb;}{;type\verb;};:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-  \type{Complex}{\Real\x \Real}
-\end{leftside}%
-\begin{rightside}
-\type{Complex}{\Real\x \Real}
-\end{rightside}
-\end{minipage}
-
-Composites types can be typeset using the {\tt composite} environment:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-  \begin{composite}{Datec}
-    day:\set{1,\ldots,366}, \\
-    year:\set{1583,\ldots,2599}
-  \end{composite}
-\end{leftside}%
-\begin{rightside}
-\begin{composite}{Datec}
-  day :\set{1,\ldots,366}, \\
-  year:\set{1583,\ldots,2599}
-\end{composite}
-\end{rightside}
-\end{minipage}
-
-There is also a {\tt composite*} environment (and an equivalent
-\cs\scompose\ control sequence) that places the entire composite
-type on a single line:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-  \begin{composite*}{Celsius}
-    \Real
-  \end{composite*}
-\end{leftside}%
-\begin{rightside}
-\begin{composite*}{Celsius}
-  \Real
-\end{composite*}
-\end{rightside}
-\end{minipage}
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-  \scompose{Celsius}{\Real}
-\end{leftside}%
-\begin{rightside}
-\scompose{Celsius}{\Real}
-\end{rightside}
-\end{minipage}
-
-`Records' can be defined using the {\tt record\/} environment:
-
-\begin{verse}
-\verb;\begin{record}{;record-type-name\verb;}; \\
-field-name \verb;:; field-type \cs\\ \\
-\dots \\
-\verb;\end{record};
-\end{verse}
-The colons are used as sub-field separators.
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-  \begin{record}{PERSON}
-    NM : \seqof{Char} \\
-    FEM : \Bool
-  \end{record}
-\end{leftside}%
-\begin{rightside}
-    \begin{record}{PERSON}
-      NM : \seqof{Char} \\
-      FEM : \Bool
-    \end{record}
-\end{rightside}
-\end{minipage}
-
-If the definition is short, you may prefer to use a short form:
-\begin{verbatim}
-        \defrecord{PERSON}{
-          NM : \seqof{Char} \\
-          FEM : \Bool
-        }
-\end{verbatim}
-
-\begin{dangerous}
-Some people prefer the field names to appear lined up on the left, some
-on the right.  If you want them to appear on the left, say
-\cs\leftRecord; if you want them on the right, say
-\cs\rightRecord.  The scope of the \cs\leftRecord\ and
-\cs\rightRecord\ commands are the current group.  By default, you
-get \cs\rightRecord.
-\end{dangerous}
-
-Updating fields of composites using the $\mu$-function can be
-specified using \cs\chg:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-  \begin{formula}
-    \chg{p}{FEM}{\Not man(q)}
-  \end{formula}
-\end{leftside}%
-\begin{rightside}
-\chg{p}{FEM}{\Not man(q)}
-\end{rightside}
-\end{minipage}
-
-Notice that the $\mu$, parentheses, comma and $\mapsto$ were inserted
-automatically.
-
-
-
-\section{How to Typeset Functions}
-
-Typesetting $\lambda$-expressions is easy:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-  \begin{formula}
-    \LambdaFn{x,y}{x^2+y^2}
-  \end{formula}
-\end{leftside}%
-\begin{rightside}
-\LambdaFn{x,y}{x^2+y^2}
-\end{rightside}
-\end{minipage}
-
-As with \cs\forall, \cs\exists\ and \cs\unique,
-\cs\LamdbaFn\ has a *-form that places the body of the function
-below and to the right:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-  \begin{formula}
-    \LambdaFn*{x,y,z}{
-      (x^2+y^2+z^2)^{\frac12}}
-  \end{formula}
-\end{leftside}%
-\begin{rightside}
-\LambdaFn*{x,y,z}{
-  (x^2+y^2+z^2)^{\frac12}}
-\end{rightside}
-\end{minipage}
-
-There is also a {\tt fn\/} (function) environment for defining named
-functions.  It has the following structure:
-\begin{verse}
-\verb;\begin{fn}{;name-of-function\verb;}{; argument-list \verb;}; \\
-\verb;\signature{;signature-of-function\verb;}; \\
-\^{optional precondition}\\
-\^{optional postcondition}\\
- body of function (a \mmexp) \\
-\verb;\end{fn};
-\end{verse}
-
-See the third page for an example.  The \cs\signature\ is optional
-and can be placed anywhere within the body---it will always be typeset
-before the body.  Useful macros within the \cs\signature\ are:
-\cs\x\ and \cs\to, which yield $\x$ and~$\to$.  Note that you can also
-enter functions defined implicitly with pre- and post-conditions; see the
-next section on how to enter them.
-
-All of the material in the section on formulas is relevant within the
-body of the function.
-
-\sloppy\sloppy
-If you frequently intersperse your function definitions with text (and you
-should), you can save some typing by using the {\tt vdmfn\/} environment.
-\cs\begin\verb;{vdmfn}; \dots \cs\end\verb;{vdmfn}; is equivalent to
-\cs\begin\verb;{vdm};\cs\begin\verb;{fn}; \dots
-\cs\end\verb;{fn};\cs\end\verb;{vdm};.
-
-The {\tt fn} environment also has a *-form that does not insert
-parentheses around the argument list.  For example:
-
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-\begin{fn*}{MP}{\term{p}\rho\sigma}
-\ldots
-\end{fn*}
-\end{leftside}\begin{rightside}
-\begin{fn*}{MP}{
-  \term{p}\rho\sigma}
-...
-\end{fn*}
-\end{rightside}
-\end{minipage}
-
-If you require the $\DEF$ symbol by itself, then you can get it by
-saying \cs\DEF.
-
-\subsection{Invariants}
-
-To typeset an invariant on a composite object, use the following
-structure:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-\begin{record}{D}
-  day : Day \\
-  year : Year
-\end{record}
-\where
-\begin{fn}{inv-D}{mk-D(d,y)}
-  is-leapyr(y) \Or d \le 365
-\end{fn}
-\end{leftside}\begin{rightside}
-\begin{record}{D}
-  day : Day \\
-  year : Year
-\end{record}
-\where
-\begin{fn}{inv-D}{mk-D(d,y)}
-  is-leapyr(y) \Or d \le 365
-\end{fn}
-\end{rightside}
-\end{minipage}
-
-
-\section{How to Typeset Operations}
-
-Operations are typeset within the {\tt op\/} environment.
-The general structure is:
-
-\begin{verse}
-\verb;\begin{op}[;\^{name-of-operation}\verb;]; \\
-\verb;\args{;\^{list-of-arguments}\verb;}; \\
-\verb;\res{;\^{result(s)}\verb;}; \\
-\verb;\ext{;\^{list-of-externals}\verb;}; \\
-\^{pre-condition} \\
-\^{post-condition} \\
-\verb;\end{op};
-\end{verse}
-
-The order of the various parts within the {\tt op} environment is not
-important; they will always be printed in a canonical style (see
-page~\pageref{op-ex} for an example).
-
-Any of \cs\args, \cs\res, \cs\ext, \^{pre-condition} or
-\^{post-condition} may be omitted.  \verb;\begin{vdmop}; is an
-abbreviation for \verb;\begin{vdm}\begin{op};;  \verb;\end{vdmop}; is an
-abbreviation for \verb;\end{op}\end{vdm};.
-
-The \^{name-of-operation} can be any one-line expression; it is
-typeset in math mode.  An alternative way of specifying the name of
-the operation is to omit the optional argument (within \verb;[];), and
-use \verb;\opname{;\^{name-of-operation}\verb;};, anywhere within the
-body of the {\tt op} environment.
-
-The \^{list-of-arguments} is a \mmexp\ that can span multiple lines;
-force a newline with \cs\\.  If present it is placed within
-parentheses.
-
-The \^{result(s)} is also any \mmexp.  It is typeset to the right of
-any arguments.
-
-The \^{list-of-externals} takes the following form:
-\begin{verse}
-\verb;\ext{;    \\
-\quad $\langle$optional \cs\Rd\ or \cs\Wr$\rangle$
-        \^{external-name(s)} {\tt :\/} \^{external-types} \cs\\ \\
-\quad $\langle$optional \cs\Rd\ or \cs\Wr$\rangle$
-        \^{external-name(s)} {\tt :\/} \^{external-types} \cs\\ \\
-\dots \\
-\verb;};
-\end{verse}
-Alternatively, if the list of externals is long (say, more than five
-lines) the {\tt externals\/} environmment can be used:
-\begin{verse}
-\verb;\begin{externals};        \\
-\quad $\langle$optional \cs\Rd\ or \cs\Wr$\rangle$
-        \^{external-name(s)} {\tt :\/} \^{external-types} \cs\\ \\
-\quad $\langle$optional \cs\Rd\ or \cs\Wr$\rangle$
-        \^{external-name(s)} {\tt :\/} \^{external-types} \cs\\ \\
-\dots \\
-\verb;\end{externals};
-\end{verse}
-\begin{dangerous}
-Some people prefer the externals identifiers to appear lined up on the
-left, some on the right.  If you want them to appear on the left, say
-\cs\leftExternals; if you want them on the right, say
-\cs\rightExternals.  The scope of the \cs\leftExternals\ and
-\cs\rightExternals\ commands are the current group.  By default,
-you get \cs\leftExternals.
-\end{dangerous}
-
-
-The \^{pre-condition} and \^{post-condition} take similar forms:
-\begin{verse}
-\verb;\pre{;\mmexp\verb;}; \\
-\end{verse}
-or
-\begin{verse}
-\verb;\begin{precond}; \\
-\mmexp \\
-\verb;\end{precond};
-\end{verse}
-and
-\begin{verse}
-\verb;\post{;\mmexp\verb;}; \\
-\end{verse}
-or
-\begin{verse}
-\verb;\begin{postcond}; \\
-\mmexp \\
-\verb;\end{postcond};
-\end{verse}
-Use the \cs\begin\dots\cs\end\ style if the \mmexp\ is longer
-than a few lines.
-All of the constructs mentioned in the section on formulas can be used
-within pre- and post-conditions.
-
-\section{Proofs}
-
-Here's an example of typesetting proofs in the ``natural deduction''
-style.
-
-\begin{proof}
-  \From E@1 \Or E@2     \\
-1   \From E@1   \\
-    \Infer E@2 \Or E@1  \` $\vee$-I(h1) \\
-2   \From E@2           \\
-    \Infer E@2 \Or E@1  \` $\vee$-I(h2) \\
-  \Infer E@2 \Or E@1    \` $\vee$-E(h,1,2)\\
-\end{proof}
-\begin{verbatim}
-        \begin{proof}
-            \From E@1 \Or E@2                           \\
-        1       \From E@1                               \\
-                \Infer E@2 \Or E@1  \by $\vee$-I(h1)    \\
-        2       \From E@2                               \\
-                \Infer E@2 \Or E@1  \by $\vee$-I(h2)    \\
-            \Infer E@2 \Or E@1      \by $\vee$-E(h,1,2) \\
-        \end{proof}
-\end{verbatim}
-
-Proofs are embedded within the {\tt proof} environment.  (A proof does
-not have to be within a {\tt vdm} environment.)  Each line of the
-proof ends with \cs\\.  Lines that begin a subproof
-have \cs\From\ after the equation number.  Lines that end a
-subproof have \cs\Infer\ after the equation number.  Other lines
-have \cs\& after the equation number (see next example).  If you
-don't need an equation number, just omit it,  but you must have one of
-either \cs\From, \cs\Infer\ or \cs\& on each proof line.
-If you want to include a justification of a particular proof line at
-the right hand end of the line, type it after a \cs\by.  \cs\by\
-is optional; you needn't include it if you don't need a justification.
-
-Points worth bearing in mind:
-\begin{itemize}
-\item   You are automatically placed in math mode after the
-        \cs\From, \cs\Infer\ or \cs\&; the math mode ends
-        at the next \cs\by\ or \cs\\.
-\item   You {\em cannot} break a line in the middle simply by using
-        \cs\\ before \cs\by; you must use separate proof lines
-        to split a formula.
-\item   You are within a {\tt tabbing} environment within a proof, so
-        you can use all the usual {\tt tabbing} commands (\cs\=,
-        \cs\>, etc.) to line things up across proof lines.  Note
-        that you will explicitly have to enter math mode again after
-        any of these commands though.
-\end{itemize}
-
-Here's another example:
-
-\begin{proof}
-  \From \forall{x\in X}{E(x); s\in X}   \\
-1 \&    \Not\exists{x\in X}{\Not E(x)}  \` $\Forall$-defn(h)\\
-2 \&    \Not\Not E(s/x) \` $\Not\Exists$-E(1,h)\\
-  \Infer E(s/x)                         \\
-\end{proof}
-\begin{verbatim}
-\begin{proof}
-  \From \forall{x\in X}{E(x); s\in X}                       \\
-1 \&    \Not\exists{x\in X}{\Not E(x)} \by $\Forall$-defn(h)\\
-2 \&    \Not\Not E(s/x)             \by $\Not\Exists$-E(1,h)\\
-  \Infer E(s/x)                                             \\
-\end{proof}
-\end{verbatim}
-
-\begin{dangerous}
-The amount of space used by the proof number can be changed by
-changing the length \cs\ProofNumberWidth.  The distance from the
-left margin to the proof number is dictated by \cs\ProofIndent.
-\end{dangerous}
-
-
-\section{Customising the Style}
-
-{\em Some people are never satisfied.}  We all know that it's true.
-In order to cater for those who aren't satisfied with the output from
-\Vdm, some attempt has been made to allow a limited degree of
-customisation by the user.  In particular, you can alter some of the
-internal spacing chosen by \Vdm, and even have your own macros called
-at chosen places within \Vdm's macros.  Naturally, you are not advised
-to try this unless you feel you have some idea of what you want, and
-what you are doing.  In this section we list the things that you can
-change, in order of increasing difficulty.
-
-\subsection{Changing the Spacing}
-
-In several places, essentially arbitrary spacings have been chosen by
-the author.  The dimensions of these spaces are given by {\em rubber
-lengths.}\footnote{See the \LaTeX\ book for an explanation of rubber
-lengths}  If you want to change any of them, use \LaTeX's
-\cs\setlength\ or \cs\addtolength\ commands.
-For example,
-\begin{verbatim}
-        \setlength{\postHeaderSkip}{13.33pt plus 2pt minus 1pt}
-\end{verbatim}
-
-\begin{dangerous}
-The {\tt plus} and {\tt minus} parts of a length let you say how much
-that length can grow or shrink by.  For example, {\tt 12pt plus 2pt
-minus 1pt} means that the length will be in the range 11--14pt, with
-12pt as its ``natural'' length.
-\end{dangerous}
-
-The spaces in question all appear around \Vdm\ items such as
-operations, and in between major parts of such items.  The names of
-the lengths should convey where they apply.  The following table lists
-all the lengths, and their default settings.  Note that an {\tt ex} is
-about the height of an ``x'' in the current font, and an {\tt em} is
-about the width of an ``M'' in the current font.
-
-\begin{center}
-\begin{tabular}{|l|l|l|}
-\hline
-\em Length              &\em Default size &\em Used within      \\
-\hline
-\cs\preOperationSkip    &2ex $+$ 0.5ex $\minus$ 0.2ex & {\tt op} env    \\
-\cs\postOperationSkip   &2ex $+$ 0.5ex $\minus$ 0.2ex   &\\
-\cs\postHeaderSkip              &.5ex $+$ .2ex $\minus$ .2ex    &\\
-\cs\postExternalsSkip   &.5ex $+$ .2ex $\minus$ .2ex    &\\
-\cs\postPreConditionSkip        &.5ex $+$ .2ex $\minus$ .2ex    &\\
-\hline
-\cs\preFunctionSkip     &2ex $+$ .5ex $\minus$ .2ex & {\tt fn} env      \\
-\cs\postFunctionSkip    &2ex $+$ .5ex $\minus$ .2ex     &\\
-\cs\betweenSignatureAndBodySkip&1.2ex $+$ .3ex $\minus$ .2ex    &\\
-\cs\betweenFunctionAndPreSkip&1.2ex $+$ .3ex $\minus$ .2ex      &\\
-\hline
-\cs\preTypeSkip &1.2ex $+$ .5ex $\minus$ .3ex & {\tt type} command      \\
-\cs\postTypeSkip        &1.2ex $+$ .5ex $\minus$ .3ex   &\\
-\hline
-\cs\preCompositeSkip    &1.2ex $+$ .5ex $\minus$ .3ex & {\tt
-composite} env  \\
-\cs\postCompositeSkip   &1.2ex $+$ .5ex $\minus$ .3ex   &\\
-\hline
-\cs\preRecordSkip               &.75ex $+$ .3ex $\minus$ .2ex & {\tt
-record} env     \\
-\cs\postRecordSkip              &.75ex $+$ .3ex $\minus$ .2ex   &\\
-\hline
-\cs\preFormulaSkip              &1.2ex $+$ .5ex $\minus$ .3ex & {\tt
-formula} env \\
-\cs\postFormulaSkip             &1.2ex $+$ .5ex $\minus$ .3ex   &\\
-\hline
-\cs\preProofSkip                &.75ex $+$ .3ex $\minus$ .2ex & {\tt
-proof} env      \\
-\cs\postProofSkip               &.75ex $+$ .3ex $\minus$ .2ex   &\\
-\hline
-\end{tabular}
-\end{center}
-
-\subsection{Controlling Line and Paragraph Breaks}
-
-\TeX\ uses the notion of {\em penalties\/} to decide where line and
-page breaks go.  Various values of penalty are used at places within
-\Vdm\ to control breaks.  To fully understand how to choose breaks,
-read {\em The \TeX{}book}.  However, put simply, penalties are whole
-numbers in the range $\minus10000$~to $10000$.  A value of $10000$
-means ``never break here,'' and a value of $\minus10000$ means
-``always break here.''  Values in between penalise or encourage
-breaking proportionally, so that, e.g.,~a value of $\minus500$
-encourages a break, but by no means forces it.  A value of zero is
-neutral.
-
-To assign to a penalty~\cs\p, write {\tt \cs\p=1000}, for example.
-The table below list the penalties used by \Vdm, and their default
-values.
-
-\begin{center}
-\begin{tabular}{|l|l|l|}
-\hline
-\em Penalty Name & Default Value & Where Used \\
-\hline
-\cs\preOperationPenalty & 0     & {\tt op} env \\
-\cs\preExternalPenalty  & 2000  & \\
-\cs\prePreConditionPenalty      & 800   & \\
-\cs\prePostConditionPenalty     & 500   & \\
-\cs\postOperationPenalty        & -500  & \\
-\hline
-\cs\preFunctionPenalty  & 0     & {\tt fn} env \\
-\cs\betweenSignatureAndBodyPenalty&500&\\
-\cs\betweenFunctionAndPrePenalty&1000&\\
-\cs\postFunctionPenalty & -500  & \\
-\hline
-\cs\preRecordPenalty    & 0     & {\tt record} env\\
-\cs\postRecordPenalty   & -100  & \\
-\hline
-\cs\preProofPenalty     & -100  & {\tt proof} env\\
-\cs\postProofPenalty    & 0     & \\
-\hline
-\cs\preFormulaPenalty   & -100  & {\tt formula} env\\
-\cs\postFormulaPenalty  & 0     & \\
-\hline
-\end{tabular}
-\end{center}
-
-
-\subsection{Unforeseen Changes}
-
-It is a truism that no matter how good the designer of a piece of
-software is, he can never foresee all of its uses.  In this case, the
-author is quite certain that people will use \Vdm\ for all sorts of
-things apart from typesetting VDM specifications.  To cater for those
-who find that \Vdm\ does almost, but not quite, what they want, a
-number of {\em hooks\/} have been left in place.  These hooks are
-macros, which at the moment do little or nothing, but which can be
-redefined by users to change the basic operation of \Vdm (see the {\tt
-vdmindex} style for one such use).  Needless to
-say, anyone wishing to redefine a hook should already be competent in
-the ways of \LaTeX\ at least, and probably \TeX\ as well.  Rather than
-trying to explain what the hooks do, and where they do it, the user
-should look through the commented version of \Vdm\ (usually stored as
-{\tt vdm.doc}) and figure it out for himself.  Below are listed all
-the provided hooks, their default definitions, and where they are used.
-
-\begin{center}\footnotesize
-\begin{tabular}{|l|l|}
-\hline
-\em Name of hook & \em Default definition \\
-\hline
-\multicolumn{2}{|c|}{{\tt op} environment} \\
-\hline
-\cs\preOperationHook
-        &\verb*;\penalty\preOperationPenalty ;\\
-\cs\betweenHeaderAndExternalsHook
-        &\verb*;\penalty\preExternalPenalty ;\\
-\cs\betweenExternalsAndPreConditionHook
-        &\verb*;\penalty\prePreConditionPenalty ;\\
-\cs\betweenPreAndPostConditionHook
-        &\verb*;\penalty\prePostConditionPenalty ;\\
-\cs\postOperationHook
-        &\verb*;\penalty\postOperationPenalty ;\\
-\hline
-\multicolumn{2}{|c|}{{\tt fn} environment} \\
-\hline
-\cs\preFunctionHook
-                &\verb*;\penalty\preFunctionPenalty ;\\
-\cs\betweenSignatureAndBodyHook
-                &\verb*;\penalty\betweenSignatureAndBodyPenalty ; \\
-\cs\betweenFunctionAndPreHook&\verb*;\vskip-\lastskip ;\\
-                &\verb;\vskip\betweenFunctionAndPreSkip ;\\
-                &\verb*;\penalty\betweenSignatureAndBodyPenalty ; \\
-\cs\postFunctionHook
-                &\verb*;\penalty\postFunctionPenalty ; \\
-\hline
-\multicolumn{2}{|c|}{{\tt record} environment} \\
-\hline
-\cs\preRecordHook
-                &\verb*;\penalty\preRecordPenalty ;\\
-\cs\postRecordHook
-                &\verb*;\penalty\postRecordPenalty ; \\
-\hline
-\multicolumn{2}{|c|}{{\tt proof} environment} \\
-\hline
-\cs\preProofHook
-                &\verb*;\penalty\preProofPenalty ;\\
-\cs\postProofHook
-                &\verb*;\penalty\postProofPenalty ; \\
-\hline
-\multicolumn{2}{|c|}{{\tt formula} environment} \\
-\hline
-\cs\preFormulaHook
-                &\verb*;\penalty\preFormulaPenalty ;\\
-\cs\postFormulaHook
-                &\verb*;\penalty\postFormulaPenalty ; \\
-\hline
-\end{tabular}
-\end{center}
-
-
-\section{Installing the \Vdm\ files}
-
-Place the file {\tt vdm.sty} in your standard directory for \LaTeX\
-style files (your system administrator will know where this is).  If
-you have the AMS fonts, change the appropriate line in {\tt vdm.sty}
-(see instructions at the head of the file).
-%If you're on a
-%UNIX\footnote{UNIX is a trademark of AT\&T} system, you can make the
-%{\tt .sty} file from the {\tt .doc} file with the command:
-%\begin{verbatim}
-%   sed -e '/^[         ]*%/d' -e 's/%.*/%/' -e '/^$/d' vdm.doc > vdm.sty
-%\end{verbatim}
-%There are two characters between the square brackets: a tab and a
-%space.  If you're on some other system, figure out an equivalent
-%command, or make the two files the same.
-
-
-\section{New \Vdm\ commands (introduced for the {\sc bsi} version)}
-
-\begin{itemize}
-  \item There is a new keyword, \cs\rem.
-  \item Operations can also have an {\em error condition\/} part, typeset
-  after the postcondition.  The error condition is placed in an {\tt
-  errcond} environment.  An alternative short form, \cs\err, is also
-  available, which works in the same way as \cs\pre\ and \cs\post.
-
-    {\emergencystretch=4pt In support of this new part, there is a hook,
-    \cs\betweenPostAndErrConditionHook, defined to be
-     \cs\penalty\ \cs\preErrConditionPenalty\ (the default penalty is
-    500).  The preceding white space is defined by
-    \cs\preErrConditionSkip\ (default .5ex $+$ .2ex $\minus$ .2ex).}
-
-  \item \cs\Others\ is an alias for \cs\Otherwise.
-  \item Sequents are supported using the {\tt sequent} command,
-  thus:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-\begin{formula}
-\sequent{A}{B}\\
-\sequent*{Truth,Beauty,eq-intr}{Truth=Beauty}
-\end{formula}
-\end{leftside}\begin{rightside}
-\sequent{A}{B}
-\sequent*{Truth,Beauty,eq-intr}
-  {Truth=Beauty}
-\end{rightside}
-\end{minipage}
-
-  \item Optional items can be typeset using \cs\Opt, thus:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-$\Opt{fred}$
-\end{leftside}\begin{rightside}
-\Opt{fred}
-\end{rightside}
-\end{minipage}
-
-  \item There are two new monadic operators, \cs\abs\ and \cs\merge.
-
-  \item A non-empty sequence type can be defined using \cs\neseqof,
-  thus:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-\begin{formula}
-\neseqof{\Nat}
-\end{formula}
-\end{leftside}\begin{rightside}
-\neseqof{\Nat}
-\end{rightside}
-\end{minipage}
-
-  \item Restricted types (those with invariants) can be typeset, with
-  or without initialisation, using \cs\ritype\ and \cs\rtype, thus:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-\rtype{Partition}{\setof{(\setof{\Nat})}}{inv-Partition(p)}
-\ritype{Dict}{\Bool \x (\mapof{Letter}{Dict})}{\true}{(\true,\emptymap)}
-\end{leftside}\begin{rightside}
-\rtype{Partition}
-  {\setof{(\setof{\Nat})}}
-  {inv-Partition(p)}
-\ritype{Dict}
-  {\Bool \x (\mapof{Letter}{Dict})}
-  {\true}
-  {(\true,\emptymap)}
-\end{rightside}
-\end{minipage}
-
-   Accompanying these commands are \cs\betweenTypeAndInvSkip\ (default
-   .5ex $+$ .3ex $\minus$ .2ex) and \cs\betweenInvAndInitSkip\
-   (same default).
-
-  \item Record types may also have invariants and initial states
-  attached, using the \cs\inv\ and \cs\init\ commands within the {\tt
-  record} environment, thus:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-\begin{record}{D}
-  day : Day \\
-  year : Year
-\inv{(mk-D(d,y)) \DEF\\
-\quad is-leapyr(y) \Or d \le 365}
-\init{day=40 \And year=1962}
-\end{record}
-\end{leftside}\begin{rightside}
-\begin{record}{D}
-  day : Day \\
-  year : Year
-\inv{(mk-D(d,y)) \DEF
-  is-leapyr(y) \Or d \le 365}
-\init{day=40 \And year=1962}
-\end{record}
-\end{rightside}
-\end{minipage}
-
-  {\emergencystretch=4pt To go with these are \cs\betweenRecordAndInvHook,
-  \cs\betweenInvAndInitHook, \cs\betweenRecordAndInvSkip\ (default
-  .5ex $+$ .2ex $\minus$ .1ex), and \cs\betweenInvAndInitSkip\
-  (same default).}
-
-\end{itemize}
-
-\section{Acknowledgements}
-
-Many people have passed on useful suggestions and comments about \Vdm\
-and this documentation; many thanks to all of them.  In particular I
-would like to acknowledge the extensive testing done by Lynn Marshall
-while preparing her thesis, and her helpful comments and ideas, and
-the numerous worthwhile discussions with Cliff Jones.  Cliff, in
-particular, deserves the highest commendation for bravery, in actually
-using these macros in his book.  Thanks to David Carlisle for helping
-with the conversion to \TeX~3.
-
-\end{document}
-
diff --git a/Master/texmf-dist/tex/latex/vdm/vdm.sty b/Master/texmf-dist/tex/latex/vdm/vdm.sty
deleted file mode 100644
index 8ff0260c04a..00000000000
--- a/Master/texmf-dist/tex/latex/vdm/vdm.sty
+++ /dev/null
@@ -1,1185 +0,0 @@
-%%% ====================================================================
-%%%  @LaTeX-style-file{
-%%%     author          = "Mario Wolczko",
-%%%     version         = "4.00",
-%%%     date            = "14 October 1994",
-%%%     filename        = "vdm.sty",
-%%%     address         = "FORMERLY AT
-%%%                        Dept of Computer Science
-%%%                        The University of Manchester
-%%%                        Oxford Road
-%%%                        Manchester M13 9PL
-%%%                        UK",
-%%%     codetable       = "ISO/ASCII",
-%%%     keywords        = "LaTeX, VDM specification language",
-%%%     supported       = "yes",
-%%%     docstring       = "LaTeX macros for typesetting VDM
-%%%                        specifications.
-%%%                        NOTE
-%%%                        Mario no longer works at Manchester
-%%%                        This is a minimal update to LaTeX2e
-%%%                        By David Carlisle",
-%%%  }
-%%% ====================================================================
-%
-%       BSI VDM documentstyle option for LaTeX
-%
-%       M. Wolczko
-%
-%
-% Dept. of Computer Science   Internet:      mario@cs.man.ac.uk
-% The University              uucp:    mcsun!uknet!man.cs!mario
-% Manchester M13 9PL          JANET:         mario@uk.ac.man.cs
-% U.K.                        Tel: +44-61-275 6146  (FAX: 6236)
-%
-% Version for LaTeX2e by David Carlisle.
-% Just constructed by removing all the old font wierdness.
-% Not tested at all!
-%
-%
-%----------------------------------------------------------------
-%
-%       Installation-dependent features
-%
-
-
-\newif\ifams@ 
-
-\ams@true
-
-\ifams@
- \RequirePackage{amsfonts}
-\fi
-
-%----------------------------------------------------------------
-%
-%       The vdm environment
-%
-% record whether we were in horizontal mode when entering...
-\newif\ifhm@
-
-\def\vdm{\ifhmode\hm@true\else\hm@false\fi
-  \@changeMathmodeCatcodes\@postUnderPenalty10000\relax}
-
-% after an \end{vdm} the next paragraph is not indented unless a \par
-% comes first (if we entered in horizontal mode).  This is a bit of a
-% kludge!
-\def\endvdm{\ifhm@\else
-  \global\let\par=\@undonoindent
-  \global\everypar={{\setbox0=\lastbox}\global\everypar={}%
-                        \global\let\par=\@@par}%
-  \fi}
-
-\def\@undonoindent{\global\everypar={}\global\let\par=\@@par\@@par}
-
-%-----------------------------------------------------------------
-%
-%       Controlling line and page breaks
-%
-% Text within the vdm environment is essentially mathematical in
-% nature, so requires special care.  Whenever outer vertical mode is
-% entered, the \@beginVerticalVDM command should be used.  This sets
-% up \leftskip, \rightskip, \baselineskip, \lineskip and
-% \lineskiplimit to conform with the overall style.
-%
-% When entering unrestricted horizontal mode, the \@beginHorizontalVDM
-% command should be used.  This sets up:
-%       \leftskip and \rightskip to 0,
-%       \\ to do line breaking
-%       ragged right line breaking, with special penalties, and
-%       enters math mode.
-% \@endHorizontalVDM should be called when leaving unrestricted
-% horizontal mode.
-
-\def\@beginVerticalVDM{\@changeMargins\@changeBaselineskip}
-
-\def\@beginHorizontalVDM{\@restoreLineSeparator
-  \@restoreMargins\@raggedRight\noindent$\strut\relax}
-\def\@endHorizontalVDM{\relax\strut$}
-
-% \VDMindent is used for \leftskip within VDM, \VDMrindent for
-% \rightskip, \VDMbaselineskip for \baselineskip
-\newdimen\VDMindent \VDMindent=\parindent
-\newdimen\VDMrindent \VDMrindent=\parindent
-\def\VDMbaselineskip{\baselineskip}
-
-\def\@changeMargins{\leftskip=\VDMindent \rightskip=\VDMrindent}
-\def\@restoreMargins{\advance\hsize by-\leftskip
-  \advance\hsize by-\rightskip
-  \leftskip=0pt \rightskip=0pt}
-\def\@changeBaselineskip{\baselineskip=\VDMbaselineskip
-  \lineskip=0pt \lineskiplimit=0pt
-  % need to alter the size of struts, too
-  \setbox\strutbox\hbox{\vrule height.7\baselineskip
-      depth.3\baselineskip width\z@}}
-
-% these are used in externals, records and cases
-\def\@changeLineSeparator{\let\\=\cr} % for usr within \halign
-\def\@restoreLineSeparator{\let\\=\newline}
-
-\def\@raggedRight{\rightskip=0pt plus 1fil
-  \hyphenpenalty=-100 \linepenalty=200
-  \binoppenalty=10000 \relpenalty=10000 \pretolerance=-1}
-
-% ------------------------------------------------------------------------
-
-%       Font and Character Changes
-
-% make a-zA-Z use the \it family within math mode, and ~ mean \hook.
-% Digits 0-9 remain as normal.
-\everymath=\expandafter{\the\everymath\vdm@it
-        \@changeMathmodeCatcodes}%
-\everydisplay=\expandafter{\the\everydisplay\vdm@it
-        \@changeMathmodeCatcodes}%
-
-\def\vdm@it{\@fontswitch\it\mathit}
-
-\mathcode`\0="0030
-\mathcode`\1="0031
-\mathcode`\2="0032
-\mathcode`\3="0033
-\mathcode`\4="0034
-\mathcode`\5="0035
-\mathcode`\6="0036
-\mathcode`\7="0037
-\mathcode`\8="0038
-\mathcode`\9="0039
-
-\mathchardef\Gamma="0000
-\mathchardef\Delta="0001
-\mathchardef\Theta="0002
-\mathchardef\Lambda="0003
-\mathchardef\Xi="0004
-\mathchardef\Pi="0005
-\mathchardef\Sigma="0006
-\mathchardef\Upsilon="0007
-\mathchardef\Phi="0008
-\mathchardef\Psi="0009
-\mathchardef\Omega="000A
-
-% If the user really wants the normal codes, she can call \defaultMathcodes
-%\def\defaultMathcodes{\let\vdm@it\relax}
-\def\defaultMathcodes{\let\vdm@it\relax}
-
-
-% remember the original mathcode of minus sign
-\edef\@minuscode{\the\mathcode`\-}
-
-\def\mathminus{\mathcode`\-=\@minuscode }
-\def\textminus{\mathcode`\-="002D }
-% by default, use text minus
-%\textminus
-
-% make a : into punctuation, a - into a letter, and | mean \mid
- % NFSS-change
- % \mathcode`\-="042D changed to \mathcode`\-="002D as we can not rely on
- % \itfam being fam 4.
- \def\@changeOtherMathcodes{\mathcode`\:="603A \textminus
-  \mathcode`\|="326A \mathchardef\Or="325F }% this is a rel to get 5mu spacing
- \def\relbar{\mathrel{\smash\minus}}% redefine because mathcode of -
-                                    % has changed
-
-
-% alternative underscore
-\def\@VDMunderscore{\leavevmode
-  \kern.06em\vbox{\hrule\@height .2ex\@width .3em}\penalty\@postUnderPenalty
-  \hskip 0.1em}
-
-% Allow line breaks after an underscore, but not in vdm mode (see
-% \vdm).  This is so long identifiers can be broken when run
-% into paragraphs.
-\newcount\@postUnderPenalty \@postUnderPenalty=200
-
-% now require some catcode trickery to enable us to change _ when we want to
-{\catcode`\_=\active 
- \gdef\@changeGlobalCatcodes{% make _ a normal char
-        \catcode`\_=\active \let_=\@VDMunderscore}
- \gdef\@changeMathmodeCatcodes{%
-        % make ~ mean \hook, " do text, @ mean subscript
-        \let~=\hook
-        \catcode`\@=8
-        \mathcode`\"="8000 }
-        \uccode`\~=`\"%
- \gdef\underscoreoff{% make _ a normal char
-        \catcode`\_=\active \let_=\@VDMunderscore}
- \gdef\underscoreon{% restore underscore to usual meaning
-        \catcode`\_=8}
-\uppercase{\gdef~}#1"{\nfss@text{\rm #1}}}
-
-%----------------------------------------------------------------
-%
-%       Keywords
-%
-\ifx\fmtname\@fmtname
-        \def\keywordFontBeginSequence{\sf}%     user-definable
-\else\ifx\fmtname\@psfmtname
-        \def\keywordFontBeginSequence{\sf}% Helvetica is OK
-\else
-        \def\keywordFontBeginSequence{\bf}% good for SliTeX
-\fi\fi
-
-\def\kw#1{\hbox{\keywordFontBeginSequence #1\/}}
-
-\def\makeNewKeyword#1#2{% use \newcommand for extra checks
-        \newcommand{#1}{\hbox{\keywordFontBeginSequence #2\/}}}
-
-\makeNewKeyword{\nil}{nil}
-\makeNewKeyword{\True}{true}
-\makeNewKeyword{\true}{true}
-\makeNewKeyword{\False}{false}
-\makeNewKeyword{\false}{false}
-\makeNewKeyword{\rem}{ rem }
-
-\def\where{\par\moveright\VDMindent\hbox{\keywordFontBeginSequence where\/}}
-
-%----------------------------------------------------------------
-%
-%       monadic operator creation
-%
-\def\newMonadicOperator#1#2{\newcommand{#1}{\kw{#2\kern.16667em}\nobreak}}
-
-%----------------------------------------------------------------
-%
-%       primitive numeric types
-%
-% use the AMS fonts for these if possible
-
-\ifams@
-  \DeclareMathSymbol{\Bool} {\mathord}{AMSb}{"42}   % Booleans
-  \DeclareMathSymbol{\Nat}  {\mathord}{AMSb}{"4E}   % Natural numbers
-  \def\Nati{\Nat_1}             % Positive natural numbers
-  \DeclareMathSymbol{\Int}  {\mathord}{AMSb}{"5A}   % Integers
-  \DeclareMathSymbol{\Real} {\mathord}{AMSb}{"52}   % Reals
-  \DeclareMathSymbol{\Rat}  {\mathord}{AMSb}{"51}   % Rationals
-\else
-  \def\Bool{\nfss@text{\bfseries B\/}}
-  \def\Nat{\nfss@text{\bfseries N\/}}
-  \def\Nati{\hbox{$\nfss@text{\bfseries N}_1$}}
-  \def\Int{\nfss@text{\bfseries Z\/}}
-  \def\Real{\nfss@text{\bfseries R\/}}
-  \def\Rat{\nfss@text{\bfseries Q\/}}
-\fi
-\let\Natone=\Nati % just for an alternative
-
-%----------------------------------------------------------------
-%
-%       Operations
-%
-% The op environment.  Within op you can specify args,
-% result, etc. which are gathered into registers, and output when the
-% op env. ends.
-%
-% The optional argument is the operation name
-
-% shorthand for an operation on its own: the vdmop env.
-\def\vdmop{\vdm\op} \def\endvdmop{\endop\endvdm}
-
-% registers constructed within an op environment
-\newtoks\@operationName
-\newbox\@operationNameBox
-\newif\ifArgumentListEncountered@
-\newtoks\@argumentListTokens
-\newtoks\@resultNameAndTypeTokens
-\newbox\@externalsBox
-\newbox\@preConditionBox
-\newbox\@postConditionBox
-\newbox\@errConditionBox
-
-\def\op{% clear temporaries, deal with optional arg
-        \setbox\@operationNameBox=\hbox{}%
-        \@argumentListTokens={}\ArgumentListEncountered@false
-        \@resultNameAndTypeTokens={}%
-        \setbox\@externalsBox=\box\voidb@x
-        \setbox\@preConditionBox=\box\voidb@x
-        \setbox\@postConditionBox=\box\voidb@x
-        \par\preOperationHook
-        \vskip\preOperationSkip
-        \@beginVerticalVDM
-        \@ifnextchar [{\@opname}{}}
-
-% breaking parameters
-\newcount\preOperationPenalty \preOperationPenalty=0
-\newcount\preExternalPenalty \preExternalPenalty=2000
-\newcount\prePreConditionPenalty \prePreConditionPenalty=800
-\newcount\prePostConditionPenalty \prePostConditionPenalty=500
-\newcount\preErrConditionPenalty \preErrConditionPenalty=500
-\newcount\postOperationPenalty \postOperationPenalty=-500
-
-% gaps between bits of operations
-\newskip\preOperationSkip \preOperationSkip=2ex plus 0.5ex minus 0.2ex
-\newskip\postOperationSkip \postOperationSkip=2ex plus 0.5ex minus 0.2ex
-\newskip\postHeaderSkip \postHeaderSkip=.5ex plus .2ex minus .2ex
-\newskip\postExternalsSkip \postExternalsSkip=.5ex plus .2ex minus .2ex
-\newskip\postPreConditionSkip \postPreConditionSkip=.5ex plus .2ex minus .2ex
-\newskip\preErrConditionSkip \preErrConditionSkip=.5ex plus .2ex minus .2ex
-
-\def\endop{% make up operation
-        % IMPORTANT---don't remove the vskips in this macro
-        % if you don't want one, set it to 0pt
-        \vskip 0pt
-        \@setOperationHeader
-        \betweenHeaderAndExternalsHook
-        \vskip\postHeaderSkip
-        \ifvoid\@externalsBox
-              \betweenExternalsAndPreConditionHook
-        \else \moveright\VDMindent\box\@externalsBox
-              \betweenExternalsAndPreConditionHook
-              \vskip\postExternalsSkip
-        \fi
-        \ifvoid\@preConditionBox
-              \betweenPreAndPostConditionHook
-        \else \moveright\VDMindent\box\@preConditionBox
-              \betweenPreAndPostConditionHook
-              \vskip\postPreConditionSkip
-        \fi
-        \ifvoid\@postConditionBox
-              \betweenPostAndErrHook
-        \else \moveright\VDMindent\box\@postConditionBox
-              \betweenPostAndErrConditionHook
-        \fi
-        \ifvoid\@errConditionBox
-        \else \vskip\preErrConditionSkip
-              \moveright\VDMindent\box\@errConditionBox
-        \fi
-        \postOperationHook
-        \vskip\postOperationSkip}
-
-% hooks for user-defined expansion
-% TeX is in outer vertical mode when these are called.
-% ALWAYS leave TeX in vertical mode after these macros have been called
-\def\preOperationHook{\penalty\preOperationPenalty }
-\def\betweenHeaderAndExternalsHook{\penalty\preExternalPenalty }
-\def\betweenExternalsAndPreConditionHook{\penalty\prePreConditionPenalty }
-\def\betweenPreAndPostConditionHook{\penalty\prePostConditionPenalty }
-\def\betweenPostAndErrConditionHook{\penalty\preErrConditionPenalty }
-\def\postOperationHook{\penalty\postOperationPenalty }
-
-% combine the operation name, argument list and result
-\def\@setOperationHeader{%
-        \moveright\VDMindent\vtop{%
-                \ifArgumentListEncountered@
-                        \setbox\@operationNameBox=%
-                                \hbox{\unhbox\@operationNameBox$($}\fi
-                \hangindent=\wd\@operationNameBox \hangafter=1
-                \noindent\kern-.05em\box\@operationNameBox
-                \@beginHorizontalVDM
-                \ifArgumentListEncountered@\the\@argumentListTokens)\fi
-                \ \the\@resultNameAndTypeTokens
-                \@endHorizontalVDM}}
-
-% set the operation name
-% \opname{name-of-operation}
-\def\opname#1{\@opname[#1]}
-\def\@opname[#1]{\@operationName={#1}%
-  \global\setbox\@operationNameBox=\hbox{$\relax#1$\ }}
-
-% set up the argument list
-% \args{ argument \\ argument \\ argument... } where \\ forces a line break
-% This is also used in the fn environment
-\def\args{\global\ArgumentListEncountered@true \global\@argumentListTokens=}
-
-% result name and type
-\def\res{\global\@resultNameAndTypeTokens=}
-
-% externals list
-%
-% An external list could be either very long or very short, so we provide
-% two forms.  One is the short \ext{..} command, the other is the externals
-% environment.
-% Externals are always separated by \\
-%
-
-% we have to mess a little to get the catcode of : right
-\def\ext{\bgroup\@makeColonActive\@ext}
-\def\@ext#1{\externals#1\endexternals\egroup}
-
-\def\externals{\global\setbox\@externalsBox=%
-        \@beginIndentedPara{\hsize}{ext }{\@setUpExternals}}
-\def\endexternals{\@endIndentedPara{\@endAlignment}}
-
-\def\@setUpExternals{\@makeColonActive\@changeLineSeparator\@beginAlignment}
-
-% more catcode trickery for :
-{\catcode`\:=\active
- \gdef\@makeColonActive{\catcode`\:=\active \let:=&}}
-
-% the \expandafters are necessary because TeX doesn't expand
-% \halign specs when scanning for # and &
-\def\@beginAlignment{\expandafter\halign\expandafter\bgroup
-        \the\@extAlign\strut\enspace&:\enspace$##$\hfil\cr}
-\def\@endAlignment{\crcr\egroup}
-
-% the user can decide on the exact alignment of the field names
-\newtoks\@extAlign
-\def\leftExternals{\@extAlign={$##$\hfil}}
-\def\rightExternals{\@extAlign={\hfil$##$}}
-\leftExternals
-
-\makeNewKeyword{\Rd}{rd } \makeNewKeyword{\Wr}{wr }
-
-% pre-condition, post-condition and err-condition
-%
-% once again we provide short forms \pre, \post, \err and environments
-% precond, postcond and errcond
-\def\pre#1{\precond#1\endprecond}
-\def\precond{\global\setbox\@preConditionBox=%
-        \@beginMathIndentedPara{\hsize}{pre }}
-\def\endprecond{\@endMathIndentedPara}
-
-\def\post#1{\postcond#1\endpostcond}
-\def\postcond{\global\setbox\@postConditionBox=%
-        \@beginMathIndentedPara{\hsize}{post }}
-\def\endpostcond{\@endMathIndentedPara}
-
-\def\err#1{\errcond#1\enderrcond}
-\def\errcond{\global\setbox\@errConditionBox=%
-        \@beginMathIndentedPara{\hsize}{errs }}
-\def\enderrcond{\@endMathIndentedPara}
-
-
-%----------------------------------------------------------------
-%
-%       Box man\oe uvres
-%
-% Here's where all the tricky box manipulation commands go
-%
-% \@beginIndentedPara begins construction of a \hbox of width #1
-% which contains keyword #2 to the left of a para in a vtop.
-% #3 is evaluated within the inner vtop.
-% endIndentedPara closes the box off; its arg. is evaluated just
-% before closing the box.
-%
-\def\@beginIndentedPara#1#2#3{\hbox to #1\bgroup \setbox0=\kw{#2}%
-        \copy0 \strut \vtop\bgroup \advance\hsize by -\wd0 #3}
-\def\@endIndentedPara#1{\strut#1\egroup\hss\egroup}
-
-% \@beginMathIndentedPara places the para in vdm mode
-\def\@beginMathIndentedPara#1#2{\@beginIndentedPara{#1}{#2}%
-        {\@beginHorizontalVDM}}
-\def\@endMathIndentedPara{\@endIndentedPara{\@endHorizontalVDM}}
-
-% \@belowAndIndent#1#2 places #2 in a vbox below and to the right of #1
-\def\@belowAndIndent#1#2{#1\hfil\break
-        \@beginMathIndentedPara{\hsize}{\qquad}#2\@endMathIndentedPara}
-
-% \@mathIndentedPara does the whole thing
-\def\@mathIndentedPara#1#2#3{\@beginMathIndentedPara{#1}{#2}#3%
-        \@endMathIndentedPara}
-%----------------------------------------------------------------
-%
-%       Constructions
-%
-% Here are all the standard constructions.
-% The only tricky one is \cases.
-% Those that construct a box must be made to make that box of 0 width,
-% and force a line break immediately afterwards.
-
-% \If mm-exp \Then mm-exp \Else mm-exp \Fi
-% multi-line indented if-then-else
-%
-\def\If#1\Then#2\Else#3\Fi{\vtop{%
-        \@mathIndentedPara{0pt}{if }{#1}%
-        \@mathIndentedPara{0pt}{then }{#2}%
-        \@mathIndentedPara{0pt}{else }{#3}}}
-
-% \SIf mm-exp \Then mm-exp \Else mm-exp \Fi
-% single line if-then-else
-\def\SIf#1\Then#2\Else#3\Fi{\hbox to 0pt{\vtop{\@beginHorizontalVDM
-        \kw{if }\nobreak#1\penalty0\hskip 0.5em
-        \kw{then }\nobreak#2\penalty-100\hskip 0.5em % break here OK
-        \kw{else }\nobreak#3\@endHorizontalVDM}\hss}}
-
-% \Let mm-exp \In mm-exp2
-% multi-line let..in ; mm-exp2 is `curried'
-\def\Let#1\In{\vtop{%
-        \@mathIndentedPara{0pt}{let }{#1\hskip 0.5em\kw{in}}}\hfil\break}
-
-% \SLet mm-exp \In mm-exp
-% single-line let..in
-\def\SLet#1\In#2{\hbox to 0pt{\vtop{\@beginHorizontalVDM
-        \kw{let }\nobreak#1\hskip 0.5em
-        \kw{in }\penalty-100 #2\@endHorizontalVDM}\hss}}
-
-% multi-line cases
-%
-% \Cases{ selecting-mm-exp }
-% from-case1 & to-case1 \\
-% from-case2 & to-case2 \\
-%           ...
-% from-casen & to-casen
-% \Otherwise{ mm-exp }
-% \Endcases[optional text for the rest of the line]
-
-\newif\ifOtherwiseEncountered@
-\newtoks\@OtherwiseTokens
-
-\def\Cases#1{\hbox to 0pt\bgroup \vtop\bgroup
-                \@mathIndentedPara{\hsize}{cases }{\strut
-                        #1\hskip 0.5em\strut\kw{of}}%
-                \bgroup % we might be in a nested case, so we have to
-                        % save the \Otherwise bits we might lose
-                \OtherwiseEncountered@false \@changeLineSeparator
-                \@beginCasesAlignment}
-
-% the user can decide on the exact alignment
-\newtoks\@casesDef
-\def\leftCases{\@casesDef={$##$\hfil}}
-\def\rightCases{\@casesDef={\hfil$##$}}
-\rightCases
-
-% the \expandafters are necessary because TeX doesn't expand
-% \halign specs when scanning for # and &
-\def\@beginCasesAlignment{\expandafter\halign\expandafter\bgroup
-        \the\@casesDef&$\,\rightarrow##$\hfil\cr}
-
-\def\Otherwise{\global\OtherwiseEncountered@true \global\@OtherwiseTokens=}
-\let\Others=\Otherwise
-
-\def\Endcases{\@endCasesAlignment \@setOtherwise \egroup \@setEndcases}
-\def\@endCasesAlignment{\crcr\egroup}
-\def\@setOtherwise{\ifOtherwiseEncountered@ % have an otherwise clause
-        \@mathIndentedPara{\hsize}{others }{%
-                \strut\the\@OtherwiseTokens\strut}
-        \fi}
-
-% must test for the optional arg to follow the end
-\def\@setEndcases{\noindent
-        \strut\kw{end}\@ifnextchar [{\@unbracket}{\@finalCaseEnd}}
-\def\@unbracket[#1]{$#1$\@finalCaseEnd}
-\def\@finalCaseEnd{\egroup\hss\egroup}%\hfil\break
-
-%----------------------------------------------------------------
-%
-%       special symbols
-
-% defined as
-\def\DEF{\raise.5ex
-        \hbox{\footnotesize\underline{$\mathchar"3234$}}}% a \triangle
-
-
-% cross product
-\let\x=\times
-
-%       logical connectives
-%
-\def\Iff{\penalty-50\mskip 7mu plus 2mu minus 2mu
-        \Leftrightarrow\mskip 7mu plus 2mu minus 2mu}
-\let\iff=\Iff
-\def\Implies{\penalty-35\mskip 6mu plus 2mu minus 1mu \Rightarrow
-        \mskip 6mu plus 2mu minus 1mu}
-\let\implies=\Implies
-% see changeOtherMathcodes for \Or
-\let\And=\land
-\let\@and=\and
-\def\and{\ifmmode\And\else\@and\fi}
-%  use \neg for logical not, or
-\def\Not{\neg\,}
-
-%       quantification
-%
-
-\DeclareMathSymbol{\Exists}   {\mathord}{symbols}{"39}
-\DeclareMathSymbol{\Forall}   {\mathord}{symbols}{"38}
-\DeclareMathSymbol{\suchthat} {\mathbin}{symbols}{"01}
-
-\def\exists{\@ifstar{\@splitExists}{\@normalExists}}
-\ifams@
-  \DeclareMathSymbol{\@nexists} {\mathop}{AMSb}{"40}
-               % crossed out existential quantifier
-\else
-  \def\@nexists{\hbox to 0pt{\raise0.15ex\hbox{/}\hss}\Exists}
-\fi
-\def\nexists{\@ifstar{\@splitNExists}{\@normalNExists}}
-\def\forall{\@ifstar{\@splitForall}{\@normalForall}}
-\def\unique{\@ifstar{\@splitUnique}{\@normalUnique}}
-\def\uniqueval{\@ifstar{\@splitUniqueval}{\@normalUniqueval}}
-
-\def\@normalExists#1#2{{\Exists#1}\suchthat #2}
-\def\@normalNExists#1#2{{\@nexists#1}\suchthat #2}
-\def\@normalForall#1#2{{\Forall#1}\suchthat #2}
-\def\@normalUnique#1#2{{\Exists!\,#1}\suchthat #2}
-\def\@normalUniqueval#1#2{{\iota\,#1}\suchthat #2}
-
-\def\@splitExists#1{\@belowAndIndent{\Exists#1\suchthat}}
-\def\@splitNExists#1{\@belowAndIndent{\@nexists#1\suchthat}}
-\def\@splitForall#1{\@belowAndIndent{\Forall#1\suchthat}}
-\def\@splitUnique#1{\@belowAndIndent{\Exists!\,#1\suchthat}}
-\def\@splitUniqueval#1{\@belowAndIndent{\iota\,#1\suchthat}}
-%
-%       sequents
-%
-\let\Tstlp=\vdash
-%
-\def\sequent{\@ifstar{\@splitSequent}{\@normalSequent}}
-\def\@normalSequent#1#2{{#1}\:\Tstlp\: #2}
-\def\@splitSequent#1{\@belowAndIndent{#1\;\Tstlp}}
-
-%
-%       strachey brackets
-%
-% (see TeXbook, p.437)
-\def\term#1{[\mkern-\thinmuskip[#1\relax]\mkern-\thinmuskip]}
-
-%       function composition
-%
-\let\compf=\circ
-
-%----------------------------------------------------------------
-%
-%       function environment
-%
-% This environment is similar to the op environment, but is used for
-% function definition.
-%
-% The mandatory first parameter is the name of the function, the
-% second is the argument list.
-%
-% The *-form simply doesn't force the parentheses round the argument list
-
-\def\fn{\parens@true\@beginVDMfunction}
-\@namedef{fn*}{\parens@false\@beginVDMfunction}
-\@namedef{endfn*}{\endfn}
-
-% short form
-\def\vdmfn{\vdm\parens@true \@beginVDMfunction}
-\def\endvdmfn{\endfn\endvdm}
-\@namedef{vdmfn*}{\vdm\parens@false \@beginVDMfunction}
-\@namedef{endvdmfn*}{\endfn\endvdm}
-
-% registers used within the fn environment
-\newtoks\@fnName
-\newbox\@fnNameBox
-\newif\ifsignatureEncountered@
-\newtoks\@signatureTokens
-\newbox\@fnDefnBox
-\newif\ifparens@
-
-\def\@beginVDMfunction#1#2{%
-        \@fnName={#1}%
-        \setbox\@fnNameBox=\hbox{$#1$}%
-        \setbox\@preConditionBox=\box\voidb@x % for people who want to do
-        \setbox\@postConditionBox=\box\voidb@x% implicit defns
-        \@signatureTokens={}\signatureEncountered@false
-        \ifparens@
-                \@argumentListTokens={(#2)}%
-        \else
-                \@argumentListTokens={#2}%
-        \fi
-        \par\preFunctionHook
-        \vskip\preFunctionSkip
-        \@beginVerticalVDM
-        \@beginFnDefn}
-
-% read in a signature
-\def\signature{\global\signatureEncountered@true \global\@signatureTokens=}
-
-\def\@beginFnDefn{\global\setbox\@fnDefnBox=\vtop\bgroup
-        \hangindent=2em \hangafter=1 \@beginHorizontalVDM
-        \advance\hsize by-2em % this fools vboxes within the
-        % function body about the hanging indent...yuk.
-        % If you change the size of the indent, change the
-        % corresponding line in \endfn.
-        \copy\@fnNameBox \the\@argumentListTokens
-        \quad\DEF\penalty-100\quad }
-
-\newskip\preFunctionSkip \preFunctionSkip=2ex plus .5ex minus .2ex
-\newskip\postFunctionSkip \postFunctionSkip=2ex plus .5ex minus .2ex
-\newskip\betweenSignatureAndBodySkip
-\betweenSignatureAndBodySkip=1.2ex plus .3ex minus .2ex
-\newskip\betweenFunctionAndPreSkip
-\betweenFunctionAndPreSkip=1.2ex plus .3ex minus .2ex
-
-\def\endfn{%
-        \advance\hsize by 2em% matches the dirty \advance in \@beginFnDefn
-        \@endHorizontalVDM
-        \egroup  % this ends the vtop we started in \@beginFnDefn
-        \ifsignatureEncountered@
-                \setbox0=\hbox{\unhbox\@fnNameBox$\;\mathpunct:\,$}%
-                \dimen255=\wd0 \noindent \box0
-                \vtop{\advance\hsize by-\dimen255 \@beginHorizontalVDM
-                        \the\@signatureTokens \@endHorizontalVDM}\par
-                \betweenSignatureAndBodyHook
-                \vskip\betweenSignatureAndBodySkip
-        \fi
-        \moveright\VDMindent\box\@fnDefnBox\,
-        \ifvoid\@preConditionBox
-              \betweenPreAndPostConditionHook
-              \vskip\postFunctionSkip
-        \else \betweenFunctionAndPreHook
-              \vskip\betweenFunctionAndPreSkip
-              \moveright\VDMindent\box\@preConditionBox
-              \betweenPreAndPostConditionHook
-              \vskip\postPreConditionSkip
-        \fi
-        \ifvoid\@postConditionBox
-              \postFunctionHook
-        \else \moveright\VDMindent\box\@postConditionBox
-              \postFunctionHook
-              \vskip\postOperationSkip
-        \fi}
-
-\newcount\preFunctionPenalty \preFunctionPenalty=0
-\newcount\betweenSignatureAndBodyPenalty
- \betweenSignatureAndBodyPenalty=10000
-\newcount\betweenFunctionAndPrePenalty \betweenFunctionAndPrePenalty=1000
-\newcount\postFunctionPenalty \postFunctionPenalty=-500
-
-% These are called in outer vertical mode---they must also exit in this mode
-\def\preFunctionHook{\penalty\preFunctionPenalty }
-\def\betweenSignatureAndBodyHook{\penalty\betweenSignatureAndBodyPenalty }
-\def\betweenFunctionAndPreHook{\penalty\betweenFunctionAndPrePenalty }
-\def\postFunctionHook{\penalty\postFunctionPenalty }
-
-%       other function-related things
-%
-
-% function arrow
-\def\to{\penalty-100\rightarrow}
-
-% explicit lamdba function
-\def\LambdaFn{\@ifstar{\@splitLambdaFn}{\@normalLambdaFn}}
-\def\@normalLambdaFn#1#2{{\lambda#1}\suchthat#2}
-\def\@splitLambdaFn#1#2{% place body in a separate box below and to the right
-        {\lambda#1}\suchthat\hfil\break
-        \@mathIndentedPara{\hsize}{\qquad}{#2}}
-
-%----------------------------------------------------------------
-%
-%       Optional fields
-%
-\def\Opt#1{\big[#1\big]}
-
-
-%----------------------------------------------------------------
-%
-%       Sets
-
-% new set type
-\def\setof#1{#1-\kw{set}}
-
-% set enumeration
-\def\set#1{\{#1\}}
-
-% empty set
-\def\emptyset{\{\,\}}
-
-% usual LaTeX operators apply: \in \notin \subset \subseteq
-\let\inter=\cap \let\intersection=\inter
-\let\Inter=\bigcap \let\Intersection=\Inter
-\let\union=\cup
-\let\Union=\bigcup
-
-\mathchardef\minus="2200
-
-\def\diff{\minus} \let\difference=\diff
-
-\newMonadicOperator{\card}{card}
-\newMonadicOperator{\Min}{min}
-\newMonadicOperator{\Max}{max}
-\newMonadicOperator{\abs}{abs}
-
-%----------------------------------------------------------------
-%
-%       Map type
-
-% new map type
-\def\mapof#1#2{#1\buildrel m\over\longrightarrow#2}
-
-% one-one map
-\def\mapinto#1#2{#1\buildrel m\over\longleftrightarrow#2}
-
-% map enumeration
-\def\map#1{\{#1\}}
-
-% empty map
-\def\emptymap{\{\,\}}
-
-%       map operators
-%
-% use \mapsto for |->
-% overwrite
-\def\owr{\dagger}
-
-\let\dres=\lhd
-\let\rres=\rhd
-
-
-% domain subtraction
-\def\dsub{\mathbin{\hbox{$\rlap{$\mathord\minus$}\mkern-1.5mu
-        \lower.1ex\hbox{$\dres$}$}}}
-
-% range subtraction
-\def\rsub{\mathbin{\hbox{$\rlap{$\mathord\minus$}\mkern-1.5mu
-        \lower.1ex\hbox{$\rres$}$}}}
-
-\newMonadicOperator{\dom}{dom}
-\newMonadicOperator{\rng}{rng}
-\newMonadicOperator{\merge}{merge}
-
-%----------------------------------------------------------------
-%
-%       Sequences
-%
-
-% new type
-\def\seqof#1{#1^*}
-
-% non-empty sequence
-\def\neseqof#1{#1^+}
-
-% enumeration
-\def\seq#1{[#1]}
-
-% empty sequence
-\def\emptyseq{[\,]}
-
-\newMonadicOperator{\len}{len}
-\newMonadicOperator{\hd}{hd}
-\newMonadicOperator{\tl}{tl}
-\newMonadicOperator{\elems}{elems}
-\newMonadicOperator{\inds}{inds}
-\def\cons#1{\kw{cons}\nobreak(#1)}
-
-% sequence concatenation
-
-\DeclareMathSymbol{\@sc@nc} {\mathbin}{AMSb}{"79}
-
-\ifams@
-  \def\sconc{\mathbin{\hbox{\raise1ex\hbox{$\@sc@nc$}}}}
-\else
-  % this is truly yukky
-  \def\sconc{\mathbin{\hbox{\raise1ex\hbox{$\frown$}\kern-0.47em
-        \raise0.2ex\hbox{\it\char"12}}}}
-\fi
-
-% distributed concatenation
-\newMonadicOperator{\Conc}{dconc}
-
-%----------------------------------------------------------------
-%
-%       type equation
-%
-\newtoks\@typeName
-\def\type#1#2{{\@typeName{#1} \preTypeHook \vskip\preTypeSkip
-        \@beginVerticalVDM
-        \moveright\VDMindent\vtop{\@beginHorizontalVDM #1=#2%
-                \@endHorizontalVDM}
-        \postTypeHook \vskip\postTypeSkip}}
-
-% restricted type (has invariant)
-\def\rtype#1#2#3{{\@typeName{#1} \preTypeHook \vskip\preTypeSkip
-        \@beginVerticalVDM
-        \moveright\VDMindent\vtop{\@beginHorizontalVDM #1=#2%
-                \@endHorizontalVDM}
-        \vskip\betweenTypeAndInvSkip
-        \moveright\VDMindent\@mathIndentedPara{\hsize}{inv }{#3}%
-        \postTypeHook \vskip\postTypeSkip}}
-
-% initialised type
-\def\ritype#1#2#3#4{{\@typeName{#1} \preTypeHook \vskip\preTypeSkip
-        \@beginVerticalVDM
-        \moveright\VDMindent\vtop{\@beginHorizontalVDM #1=#2%
-                \@endHorizontalVDM}
-        \vskip\betweenTypeAndInvSkip
-        \moveright\VDMindent\@mathIndentedPara{\hsize}{inv }{#3}%
-        \vskip\betweenInvAndInitSkip
-        \moveright\VDMindent\@mathIndentedPara{\hsize}{init }{#4}%
-        \postTypeHook \vskip\postTypeSkip}}
-
-\def\preTypeHook{} \def\postTypeHook{}
-\newskip\preTypeSkip \preTypeSkip=1.2ex plus .5ex minus .3ex
-\newskip\postTypeSkip \postTypeSkip=1.2ex plus .5ex minus .3ex
-\newskip\betweenTypeAndInvSkip
-  \betweenTypeAndInvSkip=.5ex plus .3ex minus .2ex
-\newskip\betweenInvAndInitSkip
-  \betweenInvAndInitSkip=.5ex plus .3ex minus .2ex
-
-%----------------------------------------------------------------
-%
-%       Composite Objects
-%
-
-% literal composition; we have a compose and a composite env.
-
-% single line compose
-\@namedef{composite*}#1{\kw{compose }$\relax#1\relax$\kw{ of }$\relax}
-\@namedef{endcomposite*}{\relax$\kw{ end}}
-
-% multiple line version
-\def\composite#1{\bgroup\vskip\preCompositeSkip
-    \@beginVerticalVDM
-    \moveright\VDMindent\vtop\bgroup
-        \@beginHorizontalVDM
-        \kw{compose }#1\kw{ of}%
-        \@endHorizontalVDM
-        \@makeColonActive\@changeLineSeparator
-        \expandafter\halign\expandafter\bgroup\expandafter\qquad
-                \the\@recordAlign\strut\enspace&:\enspace$##$\hfil\cr}
-\def\endcomposite{\crcr\egroup % closes \halign
-        \kw{end}\egroup % ends the \vtop
-        \vskip\postCompositeSkip\egroup}
-
-\def\scompose#1#2{\@nameuse{composite*}{#1}{#2}\@nameuse{endcomposite*}}
-
-\newskip\preCompositeSkip \preCompositeSkip=1.2ex plus .5ex minus .3ex
-\newskip\postCompositeSkip \postCompositeSkip=1.2ex plus .5ex minus .3ex
-
-% record composites; likewise we have a short and a long form
-\newtoks\@recordName
-
-\def\record#1{%
-  \InvEncountered@false \InitEncountered@false
-  \@invTokens={}\@initTokens={}
-  \@recordName{#1}
-  \par\preRecordHook
-  \vskip\preRecordSkip
-  \@beginVerticalVDM
-  \moveright\VDMindent\hbox\bgroup
-          \setbox0=\hbox{$#1$\enspace::\enspace}%
-          \@makeColonActive\@changeLineSeparator
-          \advance\hsize by-\wd0 \box0
-          \@restoreMargins
-          %
-          % the \expandafters are necessary because TeX doesn't expand
-          % \halign specs when scanning for # and &
-          \vtop\bgroup\expandafter\halign\expandafter\bgroup
-                  \the\@recordAlign\strut\enspace&:\enspace$##$\hfil\cr}
-
-\def\endrecord{\crcr\egroup% closes halign
-        \egroup% closes vtop
-        \egroup% closes hbox
-  \ifInvEncountered@
-        \betweenRecordAndInvHook
-        \vskip\betweenRecordAndInvSkip
-        \moveright\VDMindent\@mathIndentedPara{\hsize}{inv }{%
-                \the\@invTokens}
-  \fi
-  \ifInitEncountered@
-        \betweenInvAndInitHook
-        \vskip\betweenInvAndInitSkip
-        \moveright\VDMindent\@mathIndentedPara{\hsize}{init }{%
-                \the\@initTokens}
-  \fi
-  \par\postRecordHook
-  \vskip\postRecordSkip}
-
-\def\inv{\global\InvEncountered@true \global\@invTokens=}
-\def\init{\global\InitEncountered@true \global\@initTokens=}
-
-\newif\ifInvEncountered@
-\newif\ifInitEncountered@
-\newtoks\@invTokens
-\newtoks\@initTokens
-\def\betweenRecordAndInvHook{}
-\def\betweenInvAndInitHook{}
-\newskip\betweenRecordAndInvSkip
-  \betweenRecordAndInvSkip=0.5ex plus 0.2ex minus 0.1ex
-\newskip\betweenInvAndInitSkip
-  \betweenInvAndInitSkip=0.5ex plus 0.2ex minus 0.1ex
-
-% the user can decide on the exact alignment of the field names
-\newtoks\@recordAlign
-\def\leftRecord{\@recordAlign={$##$\hfil}}
-\def\rightRecord{\@recordAlign={\hfil$##$}}
-\rightRecord
-
-% more catcode trickery
-\def\defrecord{\bgroup\@makeColonActive\@defrecord}
-\def\@defrecord#1#2{\record{#1}#2\endrecord\egroup}
-
-\newskip\preRecordSkip \preRecordSkip=.75ex plus .3ex minus .2ex
-\newskip\postRecordSkip \postRecordSkip=.75ex plus .3ex minus .2ex
-\newcount\preRecordPenalty \preRecordPenalty=0
-\newcount\postRecordPenalty \postRecordPenalty=-100
-\def\preRecordHook{\penalty\preRecordPenalty }
-\def\postRecordHook{\penalty\postRecordPenalty }
-
-% \chg: mu function on composites
-\def\chg#1#2#3{\mu(#1,#2\mapsto#3)}
-
-%----------------------------------------------------------------
-%
-%       Hooks
-%
-% hooked identifiers --- these are taken from the TeXbook, p.357, 359
-\def\leftharpoonupfill{$\m@th \mathord\leftharpoonup \mkern-6mu
-  \cleaders\hbox{$\mkern-2mu \mathord\minus \mkern-2mu$}\hfill
-  \mkern-6mu \mathord\minus$}  % p.357, \leftarrowfill
-
-\def\overleftharpoonup#1{{%
-  \boxmaxdepth=\maxdimen % this fixes Lamport's figures, but isn't necessary
-                         % for versions after 15 Dec 87
-  \vbox{\ialign{##\crcr % p.359, \overleftarrow
-    \leftharpoonupfill\crcr\noalign{\kern-\p@\nointerlineskip}
-    $\hfil\displaystyle{#1}\hfil$\crcr}}}}
-
-\let\hook=\overleftharpoonup  % c'est simple comme bonjour
-
-%-----------------------------------------------------------------
-%
-%       General formula environment, a bit like \[ \] but is
-%       indented to \VDMindent and will take \\
-%
-%
-\def\form#1{\formula #1\endformula}
-
-\def\formula{\par\preFormulaHook
-        \vskip\preFormulaSkip
-        \@beginVerticalVDM
-        \bgroup
-        \moveright\VDMindent\vtop\bgroup\@beginHorizontalVDM}
-\def\endformula{\@endHorizontalVDM\egroup % ends the vtop
-        \egroup % ends the overall group
-        \par\postFormulaHook
-        \vskip\postFormulaSkip}
-
-\newskip\preFormulaSkip \preFormulaSkip=1.2ex plus .5ex minus .3ex
-\newskip\postFormulaSkip \postFormulaSkip=1.2ex plus .5ex minus .3ex
-\newcount\preFormulaPenalty \preFormulaPenalty=0
-\newcount\postFormulaPenalty \postFormulaPenalty=-100
-\def\preFormulaHook{\penalty\preFormulaPenalty }
-\def\postFormulaHook{\penalty\postFormulaPenalty }
-
-%----------------------------------------------------------------
-%
-%       Formula within a box, when width is unknown
-%
-%       equivalent to \parbox[t]{\hsize}{\@beginHorizontalVDM
-%               ...\@endHorizontalVDM}
-%
-\def\formbox{\vtop\bgroup\@beginHorizontalVDM}
-\def\endformbox{\strut\@endHorizontalVDM\egroup}
-
-%----------------------------------------------------------------
-%
-%       special font for constants
-%
-\def\constantFont{\sc}
-\def\const#1{\hbox{\constantFont{#1}\/}}
-
-%----------------------------------------------------------------
-%
-%       line break and indent
-%
-\def\T#1{\\\hbox to #1em{}}
-
-%----------------------------------------------------------------
-%
-%       line break and push line after to RHS
-%
-\def\R{\\\hspace*{\fill}}
-
-%----------------------------------------------------------------
-%
-%       Proofs
-%
-% a proof environment for typesetting proofs in the "natural
-% deduction" style.
-
-\newdimen\ProofIndent \ProofIndent=\VDMindent
-\newdimen\ProofNumberWidth \ProofNumberWidth=\parindent
-
-\def\proof{\par\preProofHook
-        \vskip\preProofSkip
-        \let\&=\@proofLine
-        \moveright\ProofIndent\vtop\bgroup
-                \@indentLevel=1
-                \advance\linewidth by-\ProofIndent
-                \begin{tabbing}%
-                \hbox to\ProofNumberWidth{}\=\kill}     % template line
-\def\endproof{\end{tabbing}\advance\linewidth by\ProofIndent
-        \egroup % ends the \vtop
-        \par\postProofHook
-        \vskip\postProofSkip}
-
-\newskip\preProofSkip \preProofSkip=1.2ex plus .5ex minus .3ex
-\newskip\postProofSkip \postProofSkip=1.2ex plus .5ex minus .3ex
-
-\newcount\preProofPenalty \preProofPenalty=-100
-\newcount\postProofPenalty \postProofPenalty=0
-\def\preProofHook{\penalty\preProofPenalty }
-\def\postProofHook{\penalty\postProofPenalty }
-
-\def\From{\@indentProof\kw{from }\=%
-        \global\advance\@indentLevel by 1
-        \@enterMathMode}
-\def\Infer{\global\advance\@indentLevel by-1
-        \@indentProof\kw{infer }\@enterMathMode}
-\def\@proofLine{\@indentProof\@enterMathMode}
-\def\by{\`}
-
-\newcount\@indentLevel
-\newcount\@indentCount
-\def\@indentProof{% do \>, \@indentLevel times
-        \global\@indentCount=\@indentLevel
-        \@gloop \>\global\advance\@indentCount by-1
-        \ifnum\@indentCount>0
-        \repeat}
-
-% need special loop macros that works in across boxes
-\def\@gloop#1\repeat{\gdef\@body{#1}\@giterate}
-\def\@giterate{\@body \global\let\@gloopNext=\@giterate
-        \else \global\let\@gloopNext=\relax \fi \@gloopNext}
-
-% this enters math mode and sets the LaTeX macros \@stopfield up
-% to exit math mode
-\def\@enterMathMode{\def\@stopfield{$\egroup}$}
-
-%----------------------------------------------------------------
-\def\VDMauthor{M.Wolczko,
-CS Dept.,
-Univ. of Manchester, UK.
-mario@cs.man.ac.uk
-uknet!man.cs!mario}
-
-\def\VDMversion{vdm3.0}
-
-\typeout{BSI VDM style option <9 Jun 1992>}
-%----------------------------------------------------------------
-%
-%       Global changes
-%
-% All things that have to be invoked before the user's stuff appears
-% should go here.
-%
-% by default the math spacing and changes to @ and _ apply everywhere
-\@changeOtherMathcodes \@changeGlobalCatcodes
-%
-%-------------------the end--------------------------------------
-\endinput
-%
-%       Summary of penalties
-%
-%       Penalties in vertical mode
-%
-% \preOperationPenalty          before an op begins
-% \preExternalPenalty           between the header and externals of an op
-% \prePreConditionPenalty       before the precondition
-% \prePostConditionPenalty      before the postcondition
-% \postOperationPenalty         at the end of an op
-%
-% \preFunctionPenalty           before a fn begins
-% \betweenSignatureAndBodyPenalty -guess
-% \postFunctionPenalty          after a fn ends
-%
-% \preRecordPenalty             before a record
-% \postRecordPenalty            after a record
-%
-%       etc for formula, proof
-%
-%       Penalties in horizontal mode in boxes
-%
-% \linepenalty                  101             \@raggedRight
-% `if mm-exp ^ then..'          0               \SIf
-% `if ... then mm-exp ^ else'   -100            \SIf
-% `let mm-exp in ^ ...'         -100            \SLet
-% `map mm-exp ^ to ...'         -50             \map
-% ^\iff                         -50             \iff
-% ^\implies                     -35             \implies
-% func(args) \DEF^              -100            \begin{fn}
-% \binoppenalty                 10000
-% \relpenalty                   10000
-% \hyphenpenalty                -100            \suchthat
-% ^\to                          -100            \to
-% _^                            100             \@VDMunderscore
-%
diff --git a/Master/texmf-dist/tpm/vdm.tpm b/Master/texmf-dist/tpm/vdm.tpm
deleted file mode 100644
index 88d4ecaf46e..00000000000
--- a/Master/texmf-dist/tpm/vdm.tpm
+++ /dev/null
@@ -1,31 +0,0 @@
-<!DOCTYPE rdf:RDF SYSTEM "../../support/tpm.dtd">
-<rdf:RDF xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" xmlns:TPM="http://texlive.dante.de/">
-  <rdf:Description about="http://texlive.dante.de/texlive/Package/vdm.zip">
-    <TPM:Name>vdm</TPM:Name>
-    <TPM:Type>Package</TPM:Type>
-    <TPM:Date>2006/01/09 00:49:07</TPM:Date>
-    <TPM:Version></TPM:Version>
-    <TPM:Creator>rahtz</TPM:Creator>
-    <TPM:Title>Typesetting VDM schemas.</TPM:Title>
-    <TPM:Description>
-The package conforms to the BSI concrete syntax for VDM, and
-enables the user to concentrate on VDM specifications rather than
-typesetting format.  Note that it does not cover all of
-BSI VDM.
-[description copied from TeX Catalogue]
-    </TPM:Description>
-    <TPM:Author>unknown</TPM:Author>
-    <TPM:Size>162394</TPM:Size>
-    <TPM:Build/>
-    <TPM:RunFiles size="40485">
-texmf-dist/tex/latex/vdm/vdm.sty
-texmf-dist/tpm/vdm.tpm
-    </TPM:RunFiles>
-    <TPM:DocFiles size="121909">
-texmf-dist/doc/latex/vdm/vdm.dvi
-texmf-dist/doc/latex/vdm/vdm.tex
-    </TPM:DocFiles>
-    <TPM:Provides>Package/vdm</TPM:Provides>
-  </rdf:Description>
-</rdf:RDF>
-