summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/tex
diff options
context:
space:
mode:
authorKarl Berry <karl@freefriends.org>2006-07-10 21:24:34 +0000
committerKarl Berry <karl@freefriends.org>2006-07-10 21:24:34 +0000
commitac151dac1f876a711cd50b4127c3c5aa8e837556 (patch)
tree622db4347270a735b6aefdf88f1b6954526665a1 /Master/texmf-dist/tex
parenta9018e6c8e9ffc9fdf4f881ab4726e90c01508d9 (diff)
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
Diffstat (limited to 'Master/texmf-dist/tex')
-rw-r--r--Master/texmf-dist/tex/latex/vdm/vdm.sty1185
1 files changed, 0 insertions, 1185 deletions
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
-%