trunk/Master/texmf-dist/source/latex/semantic

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

2 files changed, 2890 insertions, 0 deletions

diff --git a/Master/texmf-dist/source/latex/semantic/semantic.dtx b/Master/texmf-dist/source/latex/semantic/semantic.dtx
new file mode 100644
index 00000000000..28bd2c47a0c
--- /dev/null
+++ b/Master/texmf-dist/source/latex/semantic/semantic.dtx
@@ -0,0 +1,2876 @@
+%\iffalse metacomment
+%  (c)1995--2002 Peter Møller Neergaard and Arne John Glenstrup
+%  This files must be distributed, installed and used freely. You especially
+%  welcome to get inspiration (if possible) from the source code.
+%
+%  Install by running tex with "semantic.ins".  
+% 
+%  To get the documentation run latex twice on this file and then print the 
+%  file semantic.dvi.
+%
+%  This file is distributed in the hope that it will be useful,
+%  but WITHOUT ANY WARRANTY; without even the implied warranty of
+%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. 
+%\fi
+% \DeleteShortVerb{\|}
+% \CheckSum{1909}
+% \CharacterTable
+%  {Upper-case    \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
+%   Lower-case    \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
+%   Digits        \0\1\2\3\4\5\6\7\8\9
+%   Exclamation   \!     Double quote  \"     Hash (number) \#
+%   Dollar        \$     Percent       \%     Ampersand     \&
+%   Acute accent  \'     Left paren    \(     Right paren   \)
+%   Asterisk      \*     Plus          \+     Comma         \,
+%   Minus         \-     Point         \.     Solidus       \/
+%   Colon         \:     Semicolon     \;     Less than     \<
+%   Equals        \=     Greater than  \>     Question mark \?
+%   Commercial at \@     Left bracket  \[     Backslash     \\
+%   Right bracket \]     Circumflex    \^     Underscore    \_
+%   Grave accent  \`     Left brace    \{     Vertical bar  \|
+%   Right brace   \}     Tilde         \~}
+%
+% ^^A I do not want the LaTeX-commands in the index
+% ^^A This is borrowed from the standard package ``doc.dtx'' 
+% \DoNotIndex{\@,\@@par,\@beginparpenalty,\@empty}
+% \DoNotIndex{\@flushglue,\@gobble,\@input}
+% \DoNotIndex{\@makefnmark,\@makeother,\@maketitle}
+% \DoNotIndex{\@namedef,\@ne,\@spaces,\@tempa}
+% \DoNotIndex{\@tempb,\@tempswafalse,\@tempswatrue}
+% \DoNotIndex{\@thanks,\@thefnmark,\@topnum}
+% \DoNotIndex{\@@,\@elt,\@forloop,\@fortmp,\@gtempa,\@totalleftmargin}
+% \DoNotIndex{\",\/,\@ifundefined,\@nil,\@verbatim,\@vobeyspaces}
+% \DoNotIndex{\|,\~,\ ,\active,\advance,\aftergroup,\begingroup,\bgroup}
+% \DoNotIndex{\mathcal,\csname,\def,\documentstyle,\dospecials,\edef}
+% \DoNotIndex{\egroup}
+% \DoNotIndex{\else,\endcsname,\endgroup,\endinput,\endtrivlist}
+% \DoNotIndex{\expandafter,\fi,\fnsymbol,\futurelet,\gdef,\global}
+% \DoNotIndex{\hbox,\hss,\if,\if@inlabel,\if@tempswa,\if@twocolumn}
+% \DoNotIndex{\ifcase}
+% \DoNotIndex{\ifcat,\iffalse,\ifx,\ignorespaces,\index,\input,\item}
+% \DoNotIndex{\jobname,\kern,\leavevmode,\leftskip,\let,\llap,\lower}
+% \DoNotIndex{\m@ne,\next,\newpage,\nobreak,\noexpand,\nonfrenchspacing}
+% \DoNotIndex{\obeylines,\or,\protect,\raggedleft,\rightskip,\rm,\sc}
+% \DoNotIndex{\setbox,\setcounter,\small,\space,\string,\strut}
+% \DoNotIndex{\strutbox}
+% \DoNotIndex{\thefootnote,\thispagestyle,\topmargin,\trivlist,\tt}
+% \DoNotIndex{\twocolumn,\typeout,\vss,\vtop,\xdef,\z@}
+% \DoNotIndex{\,,\@bsphack,\@esphack,\@noligs,\@vobeyspaces,\@xverbatim}
+% \DoNotIndex{\`,\catcode,\end,\escapechar,\frenchspacing,\glossary}
+% \DoNotIndex{\hangindent,\hfil,\hfill,\hskip,\hspace,\ht,\it,\langle}
+% \DoNotIndex{\leaders,\long,\makelabel,\marginpar,\markboth,\mathcode}
+% \DoNotIndex{\mathsurround,\mbox,\newcount,\newdimen,\newskip}
+% \DoNotIndex{\nopagebreak}
+% \DoNotIndex{\parfillskip,\parindent,\parskip,\penalty,\raise,\rangle}
+% \DoNotIndex{\section,\setlength,\TeX,\topsep,\underline,\unskip,\verb}
+% \DoNotIndex{\vskip,\vspace,\widetilde,\\,\%,\@date,\@defpar}
+% \DoNotIndex{\[,\{,\},\]}
+% \DoNotIndex{\count@,\ifnum,\loop,\today,\uppercase,\uccode}
+% \DoNotIndex{\baselineskip,\begin,\tw@}
+% \DoNotIndex{\a,\b,\c,\d,\e,\f,\g,\h,\i,\j,\k,\l,\m,\n,\o,\p,\q}
+% \DoNotIndex{\r,\s,\t,\u,\v,\w,\x,\y,\z,\A,\B,\C,\D,\E,\F,\G,\H}
+% \DoNotIndex{\I,\J,\K,\L,\M,\N,\O,\P,\Q,\R,\S,\T,\U,\V,\W,\X,\Y,\Z}
+% \DoNotIndex{\1,\2,\3,\4,\5,\6,\7,\8,\9,\0}
+% \DoNotIndex{\!,\#,\$,\&,\',\(,\),\+,\.,\:,\;,\<,\=,\>,\?,\_}
+% \DoNotIndex{\discretionary,\immediate,\makeatletter,\makeatother}
+% \DoNotIndex{\meaning,\newenvironment,\par,\relax,\renewenvironment}
+% \DoNotIndex{\repeat,\scriptsize,\selectfont,\the,\undefined}
+% \DoNotIndex{\arabic,\do,\makeindex,\null,\number,\show,\write,\@ehc}
+% \DoNotIndex{\@author,\@ehc,\@ifstar,\@sanitize,\@title,\everypar}
+% \DoNotIndex{\if@minipage,\if@restonecol,\ifeof,\ifmmode}
+% \DoNotIndex{\lccode,\newtoks,\onecolumn,\openin,\p@,\SelfDocumenting}
+% \DoNotIndex{\settowidth,\@resetonecoltrue,\@resetonecolfalse,\bf}
+% \DoNotIndex{\clearpage,\closein,\lowercase,\@inlabelfalse}
+% \DoNotIndex{\selectfont,\mathcode,\newmathalphabet,\rmdefault}
+% \DoNotIndex{\bfdefault}
+%
+% ^^A I also exclude the commands used to generate the index
+% \DoNotIndex{\CodelineIndex,\DeleteShortVerb,\DisableCrossrefs}
+% \DoNotIndex{\EnableCrossrefs,\OnlyDescription,\RecordChanges}
+%
+% \MakeShortVerb{\"}
+%
+% \GetInfo{semantic.sty}
+% \title{The \semantic\ package\thanks
+%  {This file has version \fileversion\ and is dated
+%  \filedate.}\thanks{Michael John Downes of AMS provided a patch to
+%  make the \semantic compatible with \texttt{amsmath} v.2.01.}}
+% \author{Peter M{\o}ller Neergaard^^A
+%     \thanks{\texttt{turtle}@\texttt{turtle@linearity.org},
+%             \texttt{http://linearity.org/turtle}} \\
+%   Arne John Glenstrup^^A
+%     \thanks{\texttt{panic}@\texttt{diku.dk}, 
+%             \texttt{http://www.diku.dk/\lower0.7ex\hbox{\~{}}panic}}}
+% \maketitle
+%
+% \begin{abstract}
+%   The aim of this package is to help people doing programming
+%   languages using \LaTeX.  The package provides commands that
+%   facilitates the use of the notation of semantics and compilation
+%   in your documents. It provides an easy way to define new
+%   ligatures, \eg making "=>" a short hand for "\RightArrow".  It
+%   fascilitates the drawing of inference rules and allows you to draw
+%   T-diagrams in the "picture" environment.  It supports writing
+%   extracts of computer languages in a uniform way. It comes with a
+%   predefined set of shorthand suiting most people.
+% \end{abstract}
+%
+% ^^A Table of contents in two columns --- borrowed from the standard 
+% ^^A package of ``doc.dtx''
+% \ifmulticols
+%   \addtocontents{toc}{\protect\begin{multicols}{2}}
+% \fi
+%
+% {\parskip 0pt                ^^A We have to reset \parskip (bug in \LaTeX)
+% \sloppy
+% \tableofcontents
+% }
+%
+% \ifmulticols
+%   \begin{multicols}{2}[\noindent \medskip \rule{\textwidth}{.3pt}]
+% \fi
+% 
+% \noindent \semantic\ is a \LaTeXe\ package facilitating the writing
+% of notation of programming languages and compilation. To use it, the
+% file \texttt{semantic.sty} should be placed so that \LaTeX\ can find
+% it.
+%
+% The \semantic\ package consists of several parts, which can be used
+% independently.  The different parts are
+% 
+% \begin{description}
+% \item[Ligatures] providing an easy way to define ligatures for often used
+%   symbols like $\Rightarrow$ and $\vdash$.
+% \item[Inference Rules] fascilitating the presentation of inference rules and
+%   derivations using inference rules.
+% \item[T-diagrams] providing T-diagrams as an extension the "picture"
+%   environment.
+% \item[Reserved word\footnote{A better name is highly needed.}] fascilitating
+%   getting a uniform appearance of langugage constructions.
+% \item[Short hands] for often used symbols.
+% \end{description}
+% 
+% In the following we describe the use of the various parts of
+% \semantic and  the installation.  We also give a short introduction to the
+% two files \texttt{semantic.dtx} and \texttt{semantic.ins}.
+% 
+% This package is---like most other computer-programs---provided with
+% several bugs, insuffiencies and inconsistencies. They should be regarded
+% as features of the package. To increase the excitement of using the package
+% these features appear in unpredictable places. If they 
+% however get too annoying and seriously reduce your satisfaction with 
+% \semantic, please notify us. You could also drop us a note if you 
+% would like to be informed when \semantic\ is updated.
+% 
+% \ifmulticols
+%   \end{multicols}
+% \fi
+%
+% \iffalse^^A At the moment no bugs are known
+%   \ifmulticols
+%     \begin{multicols}{2}[\section*{Known Bugs}
+%   \fi
+%   \begin{columnItemize} 
+%   \end{columnItemize}
+%
+%   \ifmulticols
+%     \end{multicols}
+%   \fi
+% \fi
+%
+% \section{Loading}
+%
+% There is two ways of loading the \semantic\ package.  You can either load
+% it with all the parts, or to save time and space, you can load, only the
+% parts you will use.
+%
+% In the first case you just include 
+% \begin{code}
+%   "\usepackage{semantic}"  
+% \end{code}
+% in your document preamble.
+% 
+% In the other case you include
+% \begin{code}
+%   "\usepackage["\meta{parts}"]{semantic}"  
+% \end{code} 
+% in your document preamble.  \meta{parts} is a comma
+% separated list of the parts you wants to include.  The possibilities
+% are: "ligature", "inference", "tdiagram", "reserved", and
+% "shorthand".  The different parts are described in detail below.
+%
+% \section{Math Ligatures}
+% \subsection{Defining New Math Ligatures}
+% \label{sec:DefiningNewMathLigatures}
+%
+% \DescribeMacro{\mathlig} When the package is loaded, you can define new
+% ligatures for use in the math environments by using the
+% "\mathlig{"\meta{character sequence}"}{"\meta{ligature commands}"}"
+% command. \meta{character sequence} is a sequence of
+% \DeleteShortVerb{\"}\DeleteShortVerb{\|}^^A
+% characters\footnote{There are some restrictions on the characters you can
+% use. This should be described here but isn't; basically you should stick
+% to using the characters 
+% \texttt{\frenchspacing ` " ' \~{}
+% ! ? @ * ( ) [ ] < > - + = | : ; . , / 0\ldots 9}, and certainly this
+% should suffice for any sane person.}^^A
+% \MakeShortVerb{\"}
+% that must be entered in the source file to achieve the effect of the
+% \meta{ligature command}. If for example you write
+% `"\mathlig{-><-}{\rightarrow\leftarrow}"', subsequently typing `"$-><-$"'
+% will produce $\rightarrow\leftarrow$.
+%
+% \subsection{Turning Math Ligatures On and Off}
+% \label{sec:TurningMathLigaturesOnAndOff}
+%
+% \DescribeMacro{\mathligson}\DescribeMacro{\mathligsoff} By default, math
+% ligatures are in effect when the \package{mathligs} package is loaded,
+% but this can be turned off and on by using the commands "\mathligsoff" and
+% "\mathligson". Thus, typing `"$-><-$" "\mathligsoff" "$-><-$"
+% "\mathligson" "$-><-$"' 
+% will produce $\rightarrow\leftarrow$ $-{}>{}<{}-$ $\rightarrow\leftarrow$.
+%
+% \subsection{Protecting Fragile Math Commands}
+% \label{sec:ProtectingFragileMathCommands}
+%
+% \DescribeMacro{\mathligprotect} Unfortunately, some macros used in math
+% mode will break when using 
+% \package{mathligs}, so they need to be turned into protected macros with the
+% declaration "\mathligprotect{"\meta{macro}"}". \emph{NOTE:} This
+% declaration only needs to be issued once, best in the preamble.
+%
+% 
+% \section{Inference Rules}
+% 
+% \DescribeMacro{\inference}
+% \DescribeMacro{\inference*}
+% Inference rules like
+% {\def\predicatebegin#1|-#2=>#3\predicateend{$#1 \vdash \texttt{#2} \Rightarrow #3$}
+%   \[
+%     \inference[It(1) :]{\rho|-$E$=>\textsc{False}}
+%     {\rho|-while $E$ do $s$=>\rho } 
+% \quad\quad 
+%     \inference*[It(2) :]{\rho|-$E$=>\textsc{True} & \rho|-$s$=>\rho' \\
+%                \rho'|-while $E$ do $s$=>\rho''}^^A
+%     {\rho|-while $E$ do $s$=>\rho''}
+% \]}
+% and
+% \[
+%   \inference[$->*_1$]{p,\mathrm{M} ->* p',\mathrm{M'} \\ 
+%                       p',\mathrm{M'} -> p'',\mathrm{M''}}
+%       {p,\mathrm{M} ->* p'',\mathrm{M''}} \;\;\;\;
+%   \inference[$->*_2$]{}{p,\mathrm{M} ->* p,\mathrm{M}}
+% \]
+% are easily set using "\inference" and "\inference*". The syntax is 
+% \begin{code}
+%   "\inference["\meta{name}"]{"\meta{line$_1$}" \\ "\lttdots" \\ "\meta{line$_n$}"}{"\meta{conclusion}"}" 
+% \end{code}
+% and 
+% \begin{code}
+%   "\inference*["\meta{name}"]{"\meta{line$_1$}" \\ "\lttdots" \\ "\meta{line$_n$}"}{"\meta{conclusion}"}" 
+% \end{code}
+% where $n \geq 0$ so that you  can also type axioms.  When using
+% "\inference" the bar will be as wide as the conclusion and the premise,
+% whichever is widest; while "\inference*" only will make the
+% bar as wide as the conclusion (It(2) above). The 
+% optional names are typeset on the side of the inferences that they appear.
+%
+% Each line consists of premises seperated by "&":
+% \begin{code}
+%   \meta{premise$_1$}"&"\lttdots"&"\meta{premise$_m$}
+% \end{code}
+% Note that $m$ can also be zero, which is used when typing axioms. Each
+% premise and the conclusion are by default set in math mode (\see however
+% \pageref{ref:changePredicateBegin}). 
+% 
+% The rules are set so that the line flushes with the center of small
+% letters in the surrounding text. In this way, secondary conditions
+% or names (like the first example above) can be written in the
+% surrounding text. One may also set the rules in a table as shown
+% below:
+%
+%   \begin{tabular}{ll}
+%     Transitive (1): & 
+%      \inference{p,\mathrm{M} ->* p',\mathrm{M}' \\ 
+%                 p',\mathrm{M'} -> p'',\mathrm{M''}}
+%          {p,\mathrm{M} ->* p'',\mathrm{M''}} \\
+%     Transitive (2): &
+%      \inference{}{p,\mathrm{M} ->* p,\mathrm{M}}
+%   \end{tabular}
+%
+% An inference rule can  be nested within another rule without problems,
+% like in:
+% \[
+%   \inference[$->*_1$]{
+%     \inference[$->*_1$]{
+%       \inference[$->*_2$]{}
+%       {p,\mathrm{M} ->* p,\mathrm{M}} & 
+%       p,\mathrm{M} ->* p',\mathrm{M'}}
+%     {p,\mathrm{M} ->* p',\mathrm{M'}} & 
+%     p',\mathrm{M'} -> p'',\mathrm{M''}}
+%   {p,\mathrm{M} ->* p'',\mathrm{M''}}
+% \]
+%
+% \subsection{Controlling the Appearance}
+% \DescribeMacro{\setpremisesend}
+% \DescribeMacro{\setpremisesspace}
+% \DescribeMacro{\setnamespace}
+% The appearance of the inferences rules can be partly controlled by the
+% following lengths:
+% {\makeatletter
+%  \setnamespace{3em}
+%  \setpremisesend{2em}
+%  \setpremisesspace{4em}
+%  \[
+%   \inference[^^A
+%     \llap{\raisebox{0.1em}{$\overbrace{\hskip\@@nSpace}^{\makebox[0pt]{\footnotesize namespace}}$}}^^A
+%     name
+%   ]{^^A
+%     \llap{$\overbrace{\hskip\@@pEnd}^{\makebox[0pt]{\footnotesize premisesend}}$}^^A
+%     premise &
+%     \llap{$\overbrace{\hskip\@@pSpace}^{\makebox[0pt]{\footnotesize premisesSpace}}$}^^A
+%     premise
+%   }{
+%     conclusion
+%   }
+%  \]
+%  \makeatother^^A
+% }^^A
+% The lengths are changed using the three commands
+% "\setnamespace{"\meta{length}"}", "\setpremisesend{"\meta{length}"}" og
+% "\setpremisesspace{"\meta{length}"}". \meta{length} can be given in both
+% absolute units like "pt" and "cm" and in relative units like "em" and "ex".
+% The default values are: 1$\frac{1}{2}$"em" for "premisesspace",
+% $\frac{3}{4}$"em" for "premisesend" and $\frac{1}{2}$"em" for "namespace".
+% Note that the lengths \emph{cannot} be altered using the ordinary
+% \LaTeX-commands "\setlength" and "\addtolength".
+%  
+% Besides that, the appearance of inference rules is like fractions in math:
+% Among other things the premises will \emph{normally} be at same height
+% above the baseline and there is a minimum distance from the line to the
+% bottom of the premises.
+%
+% {\small ^^A This description is only for TeXnichians and it it therefore
+%         ^^A written in a smaller font.
+% \ifdanger \setparagraphmark{\small\danger} ^^A The dangorous bend is 
+%                                            ^^A designed to span two lines
+%    \parmark
+% \else 
+%   \setparagraphmark{\bfseries !!}\parmark\footnote{As your installation
+%     lacks the ``dangerous bend'' used in \emph{The \TeX\ book}, we have 
+%     used double exclamation marks to  indicate that you do not need to 
+%     understand the following paragraphs to use \semantic.}^^A
+% \fi
+% Fetching the font information from the math font and the evaluation (in
+% case they are defined in relative units) of the lengths mentioned above is
+% done just before the individual rule is set. This is demonstrated by the
+% following construction (which admittedly is not very useful):
+%
+% \smallskip
+% {\hfill
+%   \Large^^A
+%    \inference[Large]{\normalsize^^A
+%      \inference[normalsize]{\footnotesize^^A
+%       \inference[footnotesize]{\tiny^^A
+%         \inference[tiny]{}{Conclusion}}
+%        {Conclusion}}
+%      {Conclusion}}
+%    {Conclusion}\hfill}
+% \smallskip\linebreak
+% Note that  from  top to  bottom, the leaves get bigger
+% and the names get further from the line below.
+% 
+% \subsection{Formatting the Entries}
+% \parmark
+% \DescribeMacro{\predicate} 
+% To set up a single predicate (a premise or conclusion) the single-argument
+% command "\predicate" is used. This allows a finer control of the
+% formatting. As an example, all premises and conclusions can be set in
+% mathematics mode by the command:
+% \begin{code}
+%   "\renewcommand{\prediate}[1]{$ #1 $}"
+% \end{code}
+%
+% \parmark
+% \semantic\ uses "\predicate" on a premise only when the premise does not
+% contain a nested "\inference".\footnote{What \semantic\ precisely does is
+%   to append the tokens \CSname{inference} \CSname{end} to the code of a
+%   premise, when it has isolated it. \semantic\ then uses \TeX's pattern
+%   matching to search this new list of tokens for an appearance of the token
+%   \CSname{inference}. When this is found the following token is examened,
+%   and if it is \CSname{end}, \semantic\ concludes that the premise does not
+%   contain a nested inference rule} So even if the declaration above has been
+% given, "\inference" is \emph{never} be executed in math mode. Neither is
+% it used on the premises if you write:
+% \begin{code}
+%   "\inference{\inference"\lttdots"}{"\lttdots"}"
+% \end{code}
+% 
+% \parmark
+% \DescribeMacro{\predicatebegin} 
+% \DescribeMacro{\predicateend}
+% \label{ref:changePredicateBegin}
+% The default definition of "\predicate" is "\predicatebegin #1\predicateend",
+% where "\predicatebegin" and "\predicateend" are defined to `"$"'. In this
+% way the premises and conlusions are set in math
+%
+% \parmark 
+% The motivation for introducing "\predicatebegin" and "\predicateend"
+% was, however, to use \TeX's pattern matching on macro arguments to do even
+% more sophisticated formatting by redefining "\predicatebegin". 
+% \label{pattern matching}
+% If for example, \emph{every} \textsl{expression} is to be evaluated in an
+% \textsl{environment} giving a \textsl{value}, and you would like to set
+% \emph{all} the \textsl{environment's} \textsl{values} in mathematics and the
+% \textsl{expressions} in \texttt{typewriter}-font, then this could be
+% facilitated by the definition:
+% \begin{code}
+%   "\def\predicatebegin#1|-#2=>#3#4\predicateend{%" \\
+%   "  $#1 \vdash$\texttt{#2}$\stackrel{#3}{\Rightarrow}_S #4$}"
+% \end{code}\hangindent=0pt
+% Then the inference (borrowed from \textsc{M. Hennessy}, \emph{The 
+% Semantics of Programming Languages})
+% {\def\predicatebegin#1|-#2=>#3#4\predicateend{$#1 \vdash$\texttt{#2}$\stackrel{#3}{\Rightarrow}_S #4$}
+% \[
+%   \inference[TlR]{D |- $s$ =>{v} s' & D |- $s$ =>{v'} s''}
+%     {D |- Tl($s$) =>{v'} s''}
+% \]}^^A
+% can be accomplished by
+% \begin{code}
+%   "\inference[TlR]{D |- $s$ =>{v} s' & D |- $s$ =>{v'} s''}" \\
+%   "  {D |- Tl($s$) =>{v'} s''}"
+% \end{code} 
+% Please note that the "ligatures" option \emph{has not} been used
+% above. } 
+% ^^A TeXnichian mode OFF
+%
+% \section{T-diagrams}
+%
+% \DescribeMacro\compiler
+% \DescribeMacro\interpreter
+% \DescribeMacro\program
+% \DescribeMacro\machine
+% To draw T-diagrams describing the result of using one or more
+% compilers, interpreters etc., \semantic\ has commands for the diagram:
+% \begin{center}
+%   \begin{picture}(280,40)
+%     \put(10,0) {\program{P,L}}
+%     \put(70,0){\interpreter{S,L}}
+%     \put(160,0){\compiler{S,M,T}}
+%     \put(250,11.45){\machine{M}}
+%   \end{picture}
+% \end{center}
+% These commands should only be used in a "picture" environement and are
+% \begin{code}
+%   "\program{"\meta{program}","\meta{implementation language}"}" \\
+%   "\interpreter{"\meta{source}","\meta{implemenation language}"}" \\
+%   "\compiler{"\meta{source}","\meta{machine}","\meta{target}"}" \\
+%   "\machine{"\meta{machine}"}"
+% \end{code}
+% The arguments can be a either a string describing the language (please do
+% not begin the string with a  macro name), or one of the four commands.
+% However, combinations taht make no sense---like implementing an
+% interpreter on a program---are excluded, yielding an error message like:
+% \begin{code}
+% \begin{verbatim}
+% ! Package semantic Error: A program cannot be at the bottom .
+% 
+% See the semantic package documentation for explanation.
+% Type  H <return>  for immediate help.
+%  ...                                      
+% \end{verbatim}
+% \end{code}
+% 
+% When you are use a command as an argument \semantic, will copy the
+% language from the nested command and automaticly place the two figures in
+% proportion to each other. In this way, big T- diagrams can easily be
+% drawn. The hole construction should be placed using af "\put" command,
+% where the \emph{reference point} is the center of the bottom of the figure
+% corresponding to the outermost command. An example (with the
+% reference point marked by
+% \raisebox{.5ex}[0pt][0pt]{\begin{picture}(6,0)(-3,0)\put(0,0){\circle*{3}}\end{picture}})
+% will clarify some of these point.  The figure
+% \begin{center}
+%   \begin{picture}(220,75)(0,-35)
+%      \put(10,0){\interpreter{S,L'}}
+%      \put(10,0){\circle*{3}}
+%      \put(110,0){\program{P,\compiler{C,\machine{M},\program{P,M}}}}
+%      \put(110,0){\circle*{3}}
+%   \end{picture}
+% \end{center}
+% is obtained by the commands
+% \begin{code}
+%   "\begin{picture}(220,75)(0,-35)" \\
+%   " \put(10,0){\interpreter{S,L'}}" \\
+%   " \put(110,0){\program{P,\compiler{C,\machine{M},\program{P,M}}}}" \\
+%   "\end{picture}"
+% \end{code}
+% Note from the second example that when "\compiler" is used as
+% ``implementation language''-argument it is by convention attributed to the
+% right of the figure. It is also worth mentioning that there is no strict
+% demand on which command you should choose as the outermost, \emph{ie} the 
+% second example could also be written (with a change of the parameters of 
+% "\put" due to the new reference point) as
+% \begin{code}
+%   "\put(160,-20){\compiler{\program{P,C},\machine{M},\program{P,M}}}"
+% \end{code}
+% starting off in the middle instead of using a
+% ``left-to-right''-approach.  In fact,  it is  often easier to start in
+% the middle, since this is where you get the least levels of nesting.
+% 
+% Even though most situations may be handled by means of nesting, it is in
+% some rare cases adequate to use different 
+% language symbols on the two sides of the line of touch.
+% When \emph{eg} describing bootstrappring the poor U-code
+% implementation can be symbolized by \texttt{U$^{-}$}, indicating that the
+% poor implementation is still executed on a  \texttt{U}-machine. This can
+% be done by providing the symbol-command 
+% with an optional argument immediately after the command name. Thus
+% the bootstrapping
+% \begin{center}
+%   \begin{picture}(230,100)(-90,-20)
+%     \put(0,0){\compiler{\compiler{ML,ML,U},\machine[U$^{-}$]{U},\compiler{\compiler{ML,ML,U},\machine[U$^{-}$]{U},\compiler{ML,U,U}}}}
+%   \end{picture}
+% \end{center}
+% is typed 
+% \begin{code}
+%  "\compiler{\compiler{ML,ML,U},\machine[U$^-$]{U},\compiler{"\\
+%  "     \compiler{ML,ML,U},\machine[U$^-$]{U},\compiler{ML,U,U}}}"
+% \end{code}
+%
+% For calculating the dimensions of the "picture"-environment, one needs the
+% dimensions of the individual figures.  In  units of  
+% "\unitlength" they are the following:
+%
+% \ifmulticols
+%   \begin{multicols}{2}
+% \fi \noindent
+%   compiler: 80*40 \\
+%   interpreter: 20*40 \\
+%   machine: 20*17.1 \\
+%   program: 20*40
+% \ifmulticols
+%   \end{multicols}
+% \fi
+%
+% \section{Reserved Words}
+% \label{sec:Reserved Words}
+%
+% ^^A \tracingmacros=1 \tracingonline=1
+% \reservestyle{\command}{\mathbf}     \command{let,in}
+% \reservestyle{\punctuation}{\mathtt} \punctuation{=}
+% \tracingmacros=0
+%
+% When describing computer languages, one often wants to typeset commands in
+% one style, expressions in another style, and punctuation characters in
+% yet another style, for instance
+% \[
+%   \<let> \; x \;\<=>\; e \;\<in>\; e
+% \]
+%
+% \DescribeMacro{\reservestyle}
+% The \semantic\ package supports this by allowing you to reserve a certain
+% \emph{style} for certain language constructs.  The fundamental command is
+% \begin{code}
+%   "\reservestyle{"\CSname{\meta{stylename}}"}{"\meta{formatting}"}"
+% \end{code}
+% "reservestyle" reserves \CSname{\meta{stylename}} as the macro to define
+% the language constructs.  The language constructs will be set using
+% \meta{formatting}. 
+% 
+% The reserved macro \CSname{\meta{stylename}} should be given a comma
+% separated list of words to reserve.  For instance to reserve the words
+% $\<let>$ and $\<in>$ as  
+% commands, which all are set using a bold font, you can put
+% \begin{code}
+%   "\reservestyle{\command}{\textbf}" \\
+%   "\command{let,in}"
+% \end{code}
+% in the preamble of your document.  Note that there must not any
+% superfloues space in the comma separated list.
+% Thus for instance \verb*+\command{let , in}+
+% would reserve $\setcommand{let\ExplicitSpace}$ resp.\
+% $\setcommand{\ExplicitSpace in}$ instead of $\<let>$ resp. $\<in>$!
+% You can of course reserve several styles
+% and reserve several words within each of the styles.
+%  
+% \DescribeMacro{\<}
+% To refer to a \emph{reserved word} in the text you use the command
+% "\<"\meta{reserved word}">", \eg "\<let>".  If you have reserved several
+% styles, \semantic will find the style that was used to reserve
+% \meta{reserved word} and use the appropriate formatting commands.
+% 
+% The "\<"$\cdots$">" can be used in both plain text and in math mode.  You
+% should, however, decide in the preamble if a given style should be used in
+% math mode or in plain text, as the formatting commands will be different.
+%  
+% \DescribeMacro{\set\protect\meta{style}}
+% If you only want to type  a reserved word a single time, it can seem tedious
+% first to reserve the word  and then refer to it once using "\<"$\cdots$">".
+% Instead you can use the command "\set"\meta{style} that is defined for each
+% style you reserve.
+%  
+% \subsection{Bells and Whistles: Spacing in Math Mode}
+% 
+% In many situations it seems best to use \emph{reserved words} in math
+% mode---after all you get typesetting of expressions for free.  The drawback
+% is that it becomes more difficult to get the space correct.  One can of
+% course allways insert the space by hand, \eg "$\<let>\; x=e \;\<in>\; e'$",
+% However, this soon becomes tedious and \semantic have several ways to try to
+% work around this.
+% 
+% The first option is to provide "\reservestyle" with an optional spacing
+% command, \eg "\mathinner".  For instance
+% \begin{code}
+%   "\reservestyle[\mathinner]{\command}{\mathbf}"
+% \end{code}
+% will force all \emph{commands} to be typeset with spacing of math inner
+% symbols.
+% 
+% You can also provide an optional space command to each reservation of 
+% words.  For instance 
+% \begin{code}
+%   "\command[\mathrel]{in}"
+% \end{code}
+% will make $\<in>$ use the spacing of the relational symbols.  The space
+% command is applied to all the words in the reservation.  Thus if you would
+% like $\<in>$ and $\<let>$ to have different space commands, you must
+% specify them in two different "\command".
+% 
+% The drawback of using the math spacing is that in the rare cases where you
+% use the reserved words in super- or subscripts, most of the spacing will
+% disappear.  This can be avoided by defining the replacement text to be the
+% word plus a space, \eg "\;in\;".  For this end a reservation of a word can
+% be followed by an explicit replacement text in brackets, \eg
+% \begin{code}
+%   "\command{let[let\;], in[\;in\;]}"
+% \end{code}
+% The formatting of "\command" (with the setting above: "\mathbf") will still
+% be used so it is only necessary to provide the replacement text.  Note
+% that each word in the reservation can have its own optional replacement
+% text.
+%
+% The drawback of this method is, that the you also get the space, if you use
+% the reserved word ``out of context'', for instance refering to the
+% $\;\<in>\;$-token!  In these cases you can cancel the space by hand using
+% "\!".  
+%
+% This option is also usefull, if you want to typeset the same word in two
+% different styles.  If you for instance sometimes want `let' to be typeset
+% as a command and sometimes as data, you can define
+% \begin{code}
+%   "\command{let}" \\
+%   "\data{Let[let]}"  
+% \end{code}
+% Then "\<let>" will typeset the word `let' as a command, while "\<Let>" will
+% typeset it as data.  Note that in both cases the word appears in
+% lower case.
+% 
+% Unfortunately there is no way to get the right spacing everytime, so you
+% will have to choose which of the two methods serves you the best.
+%
+% \section{Often Needed Short Hands}
+% 
+% Within the field of semantics there are a tradition for using some special.
+% symbols.  These are provided as default as short hand in the \semantic\
+% package.  Most of the following symbols are defined as ligatures, and
+% hence the "ligature" option is always implied when the "shorthand" option
+% is provided.
+%
+% \makeatletter
+% \subsection{The Meaning of: \@bblb\ and \@bbrb}
+% \marginpar{\raggedleft\strut\@bblb}
+% \marginpar{\raggedleft\strut\@bbrb}
+%
+% The symbols for denoting the meaning of an expression, 
+% \@bblb\ and \@bbrb\ are provided as short
+% hands in math with the ligatures "|[" and "|]".
+% \makeatother 
+%
+% \subsection{Often Needed Symbols}
+% 
+% The following ligatures are defined for often needed symbols
+%
+% \begin{tabular}[c]{cl@{\qquad\qquad}cl}
+%   $\vdash$   & "|-"   & $\mathligsoff\models$  & "|="   \\
+%   $<->$  &  "<->"     & $<=>$  &  "<=>" \\
+%   $->$   & "->"       & $-->$  &  "-->" \\
+%   $=>$   & "=>"       & $==>$  &  "==>" \\
+%   $<-$   & "<-"       & $<--$  &  "<--" \\
+%   $<=$   & "<="       & $<==$  &  "<==" \\
+% \end{tabular}
+%
+% All the single directed arrows also comes in a starred and plussed form, \eg\
+% "*<=" gives $*<=$ and "-->+" gives $-->+$.
+%
+% \DescribeMacro{\eval} 
+% \DescribeMacro{\comp} 
+% To support writing denotational, semantics the commands "\comp" and "\eval"
+% are provided to describe the evaluation of programs respectively
+% expressions. They have the same syntax:
+% "\comp{"\meta{command}"}{"\meta{environment}"}", which yields
+% \comp{\meta{command}}{\meta{environment}}.  If you need to describe more
+% than one kind of evaluations, e.g.\ both \evalsymbol\ and \evalsymbol[*],
+% you can provide an optional argument immediately after "\comp" or
+% "\eval", respectively. As an example a denotational rule for a
+% sequencing two commands
+% \[
+% \comp{C1 ; C2}{d} = \mathtt{d'} \quad \texttt{if $\comp{C1}{d} = \mathtt{d''}$ and $\comp{C2}{d''} = \mathtt{d'}$}
+% \]
+% can be typed
+% \begin{code}
+%   "\["\\
+%   "  \comp{C1 ; C2}{d} = \mathtt{d'} \quad "\\
+%   "   \texttt{if $\comp{C1}{d} = \mathtt{d''}$ and"\\
+%   "              $\comp{C2}{d''} = \mathtt{d'}$}"\\
+%   "\]"
+% \end{code}
+% 
+% \DescribeMacro{\evalsymbol}
+% \DescribeMacro{\compsymbol}
+% As shown above, you can get the evaluation symbol in itself. This is done by
+% "\compsymbol" or  "\evalsymbol", respectively. These commands can also be
+% supplied with an optional argument, e.g.\ "\evalsymbol[*]" to get
+% \evalsymbol[*].
+% 
+% \DescribeMacro{\exe} The result of executing a program on a machine
+% with som data can be described using "\exe", which has the syntax
+% "\exe{"\meta{program}"}["\meta{machine}"]{"\meta{data}"}", where
+% \meta{machine} is optional. The third Futumara projection
+% $\mathtt{cogen} = \exe{spec}{spec.spec}$ can be written
+% "$\mathtt{cogen} = \exe{spec}{spec.spec}$". As an alternative, you
+% can also give the machine \texttt{L} explicit:
+% \begin{code} 
+%   "$\mathtt{cogen} = \exe{spec}[L]{spec.spec}$"
+% \end{code}
+%  This will result in:
+% $\mathtt{cogen} = \exe{spec}[L]{spec.spec}$
+%
+% \section{Some Notes about the Files}
+% 
+% \semantic\ is distributed in two files, "semantic.dtx" and
+% "semantic.ins".  Of these two files, "semantic.dtx" is the most
+% important, as it contains all the essentials---users guide, code and
+% documentation of the code.  "semantic.ins" is used only to guide
+% \package{docstrip} in generating "semantic.sty" from "semantic.dtx".
+% 
+% {\makeatletter To get \@bblb\ and \@bbrb, used in "\comp", "\eval" and "\exe"
+%   \semantic, tries to load the package \package{bbold} written by 
+%   \textsc{A. Jeffrey}. If this is not installed on your system, the symbols
+%   are simulated by drawing together two sharps. However, we  recommend 
+%   that you get \package{bbold} from your nearest CTAN-archive. 
+% \makeatother}
+% 
+% In addition to the users guide, you can also get the fully documented code.
+% You need this, however, if you want to see how the macros are implemented
+% the macros or if you want to change some part of the package. You should
+% start by editing "semantic.dtx", change the two lines (near line~3320)
+% \begin{code}
+%   "\OnlyDescription    % Make to a comment to get the documentation"\\
+%   "\DisableCrossrefs   % Remove comment if the index is ready or if"\\
+% \end{code}
+% into a comment, and remove "%" from the begining of the next two lines:
+% \begin{code}
+%   "%\CodelineIndex      % Make a index of the command usage"\\
+%   "%\RecordChanges      % Make the changes history"
+% \end{code}
+% Then you should run \LaTeX\ twice on the edited file to get a correct table
+% of contents. Then you generate the index and change history, using
+% "makeindex":
+% \begin{code}
+%   "makeindex -s gind.ist semantic" \\
+%   "makeindex -s gglo.ist -o semantic.gls semantic.glo"
+% \end{code}
+% After another run of \LaTeX, then the documentation is ready for printing.
+% 
+% "semantic.dtx" is designed to be used with \package{doc} and
+% \package{docstrip}. It therefore contains the package code but most
+% of it is a lot of comments.  These comments constitute the users
+% guide and the documentation of the code. When \TeX\ is runned on
+% "semantic.ins", \package{doc} is used to remove all these comments,
+% and the result is written in the package file "semantic.sty". When
+% you make the users guide by running \LaTeX\ on "semantic.dtx",
+% \LaTeX\ first skips about 815 lines of comments (containing the
+% source of the users guide) before it gets to the lines normally
+% making up the package file. Then follows nearly 2400~lines of intermixed
+% comments and code defining the commands in the package. At last,
+% \LaTeX\ arrives at a line "\documentclass{ltxdoc}" (\package{ltxdoc}
+% is \LaTeXe's standard class for documenting). After a couple of
+% packages loadings and some command definition, it reaches
+% "\begin{document}" and "\docinput{semantic.dtx}". This makes \LaTeX\
+% read over "semantic.dtx" once more but this time skipping the
+% \%-chars in the first column.
+% 
+% \medskip
+% \parmark[\copyright]^^A
+% At last the boring formal stuff: The package is protected by the The
+% \LaTeX\ Project Public License (lppl). You are encouraged to copy, use, delete
+% etc.\ the package ("semantic.dtx" and "semantic.ins") as much as
+% your heart, but if you modify the code (even locally), you should
+% change the name to avoid confusion.  Under all circumstances, the
+% package is still: {\small \copyright 1995--2000 Peter Møller Neergaard
+% and Arne John Glenstrup.}
+% 
+% \StopEventually{
+%  \ifmulticols
+%    \addtocontents{toc}{\protect\end{multicols}}
+%  \fi
+% }
+%
+% \section{Documentation of the Package Code}
+%
+% \ifmulticols
+%   \begin{multicols}{2}[\subsection{To Be Done (in Priority)}]
+% \else
+%   \subsection{To Be Done (in Priority)}
+% \fi
+% \changes{1.0}{1995/10/18}{Introduced a list of things to be done}
+% \begin{columnItemize}
+% \item Add a grammar option if needed.
+% \item If at all possible, add a check for the existence of "manfnt.tfm".
+% \item Use "\hrule" and "\vrule" instead of "\line" (cf.\ \package{Epic}) as
+%   much as possible to build the translation diagrams , since this will
+%   improve performance.
+% \item Develop example macros that set an example and give the source text
+%   for the example.
+% \item Analyze my use of registers to see if I can reduce the
+%   number of permanently reserved registers.
+% \end{columnItemize}
+% 
+% \ifmulticols
+%   \end{multicols}
+% \fi
+% 
+% \subsection{Stub for Users Guide and Documentation}
+%
+% First comes a little hack that makes \LaTeX\ think it is loading the
+% package \texttt{semantic.sty}.  In this way, the commands in the package can
+% be for printing the documentation:
+%    \begin{macrocode}
+%<*documentation>
+\makeatletter 
+\def\@currname{semantic}
+\def\@currext{sty} 
+%</documentation>
+%    \end{macrocode}
+% "\@currname" and "\@currext" is internal \LaTeX-macros containg the name
+% and extension of the package currently being loaded.  The code is
+% encapsulated in "<*documentation>"\lttdots"</documentation>".  Thus it is
+% not included in the style file, when the package is installed.
+%
+% \changes{2.0}{1995/05/24}{Added code for loader of different package options}
+%
+% \subsection{Package Identification and Option Loading}
+%
+% The package code starts by identifying the file as a \LaTeXe\ package:
+%    \begin{macrocode}
+%<*general>
+\NeedsTeXFormat{LaTeX2e} 
+\ProvidesPackage{semantic}
+  [2000/08/03 v2.0(gamma) Semantic Package]
+%</general>
+%    \end{macrocode}
+%
+% \subsubsection{Avoid Naming Conflicts}
+% 
+% The following code is used to test that all names used by the
+% \semantic-package are not used by other packages.
+%
+% \begin{macro}{\@semanticNotDefinable}
+%   \changes{2.0$\alpha$}{1996/05/18}{Added redefinition of
+%     \CSname{@notdefinable} during package loading}
+%   This replaces the internal \LaTeX\ command "\@notdefinable", which is
+%   used to issue an error message when a command cannot be defined, during
+%   loading of \semantic.  The name of the command that could not be defined
+%   is saved by \LaTeX\ in "\reserved@a".
+%    \begin{macrocode}
+%<*general>
+\newcounter{@@conflict}
+\newcommand{\@semanticNotDefinable}{%
+  \typeout{Command \@backslashchar\reserved@a\space already defined}
+  \stepcounter{@@conflict}} 
+\newcommand{\@oldNotDefinable}{}
+\let\@oldNotDefinable=\@notdefinable
+\let\@notdefinable=\@semanticNotDefinable
+%    \end{macrocode}
+%   The macro types the name of the confliction macro to the user and then 
+%   marks that there has been a conflict by increasing the numbers of
+%   conflicts encountered.  "\@notdefinable" is an internal \LaTeX\
+%   command used to write an error message when a command cannot be
+%   defined.  It is temporarily saved for later restoring.
+% \end{macro}
+%
+% \begin{macro}{\TestForConflict}
+%   \changes{2.0$\alpha$}{1996/05/18}{Added macro for testing for conlict
+%     instead of using \CSname{newcommand}}
+%   "\@testconflict" takes a list of macros (separated by comma) and testes
+%   that they are all undefined. If one of them is not undefined an error
+%   message will be issued.  The syntax is choosen like "\DoNotIndex" from
+%   \package{ltxdoc}.
+%    \begin{macrocode}
+\newcommand{\TestForConflict}{}
+\def\TestForConflict#1{\@test #1,,}
+%    \end{macrocode}
+%   The macro initialises the testing and then uses "\@test" to test the
+%   indiviual commands in the list.  
+% \end{macro}
+%
+% \begin{macro}{\@test}
+% \begin{macro}{\@stest}
+%   This is the command for doing the test of a single macro
+%    \begin{macrocode}
+\newcommand{\@test}{} \newcommand{\@temp}{} \newcommand{\@@next}{}
+\def\@test#1,{%
+  \def\@temp{#1}%
+  \ifx \@temp\empty \let\@@next=\relax \else 
+    \@ifdefinable{#1}{} \let\@@next=\@test \fi
+  \@@next}
+%</general>
+%    \end{macrocode}
+%   The macro takes a single argument. If its not empty, \ie\ the list has
+%   not been read to the end, the internal \LaTeX\ command "\@ifdefinable"
+%   is used to test if the command can be defined (\see\
+%   \cite[p.~192]{LaTeXbook}). "\@stest" is used to remove spaces in front
+%   of the argument
+% 
+%   To avoid to many unclosed "\if" the macro is made tail recursive by
+%   saving the next macro in "\@next".
+% \end{macro}
+% \end{macro}
+%
+% \subsubsection{Hack for the documentation}
+%
+% The following is a hack inserted to make the processing of the
+% documentation, skip all the options loading and just incorporate the
+% package code. 
+%    \begin{macrocode}
+%<*documentation>
+\iftrue\iffalse
+%</documentation>
+%    \end{macrocode}
+% The "\iftrue" matches the "\fi" in the bottom of the code, while the
+% "\iffalse" is skipping the code controlling loading of the options.
+%
+% \subsubsection{Loading of Options}
+%
+% The code to load the different options is defined.  By ``erasing'' the
+% definitions after loading the parts, the code ensures that no part is
+% loaded more than once.
+%    \begin{macrocode}
+%<*general>
+\TestForConflict{\@inputLigature,\@inputInference,\@inputTdiagram}
+\TestForConflict{\@inputReservedWords,\@inputShorthand}
+\TestForConflict{\@ddInput,\sem@nticsLoader,\lo@d}
+\def\@inputLigature{\input{ligature.sty}\message{ math mode ligatures,}%
+                     \let\@inputLigature\relax}
+\def\@inputInference{\input{infernce.sty}\message{ inference rules,}%
+                     \let\@inputInference\relax}
+\def\@inputTdiagram{\input{tdiagram.sty}\message{ T diagrams,}%
+                     \let\@inputTdiagram\relax}
+\def\@inputReservedWords{\input{reserved.sty}\message{ reserved words,}%
+                     \let\@inputReservedWords\relax}
+\def\@inputShorthand{\input{shrthand.sty}\message{ short hands,}%
+                     \let\@inputShorthand\relax}
+%    \end{macrocode}
+% Token register~1 is used for keeping the commands to load the package.
+% An empty register will mark that all options should be loaded:
+%    \begin{macrocode}
+\toks1={}
+%    \end{macrocode}
+% \begin{macro}{\@ddInput}
+%   "\@ddInput" adds its argument to the list of commands used for loading:
+%    \begin{macrocode}
+\newcommand{\@ddInput}[1]{%
+  \toks1=\expandafter{\the\toks1\noexpand#1}}
+%    \end{macrocode}
+%   The "\expandafter" makes "\the" expand the tokens register~0 one level,
+%   thus listing all the loading instructions.
+% \end{macro}
+%
+% Each option add the code to load the option to token register~0.
+%    \begin{macrocode}
+\DeclareOption{ligature}{\@ddInput\@inputLigature}
+\DeclareOption{inference}{\@ddInput\@inputInference}
+\DeclareOption{tdiagram}{\@ddInput\@inputTdiagram}
+\DeclareOption{reserved}{\@ddInput\@inputReservedWords}
+\DeclareOption{shorthand}{\@ddInput\@inputLigature 
+   \@ddInput\@inputShorthand}
+%    \end{macrocode}
+%
+% The options are processed
+%    \begin{macrocode}
+\ProcessOptions*
+%    \end{macrocode}
+%
+% and the specified options are loaded (if no options are specifieed, then
+% all options are loaded) 
+%    \begin{macrocode}
+\message{Semantic Package.^^JLoading}
+\def\sem@nticsLoader{}
+\edef\lo@d{\the\toks1}
+\ifx\lo@d\empty
+  \@inputLigature
+  \@inputInference
+  \@inputTdiagram
+  \@inputReservedWords
+  \@inputShorthand
+\else
+  \lo@d
+\fi
+\message{and general definitions.^^J}
+%    \end{macrocode}
+% "\sem@nticsLoader" is flag used for testing in the options file to check
+% that the files are loaeded from the package.
+%
+% After loading the options the name space is cleaned up.
+%    \begin{macrocode}
+\let\@ddInput\relax
+\let\@inputInference\relax
+\let\@inputLigature\relax
+\let\@inputTdiagram\relax
+\let\@inputReservedWords\relax
+\let\@inputShorthand\relax
+\let\sem@nticsLoader\realx
+\let\lo@d\relax
+%</general>
+%    \end{macrocode}
+% 
+% \subsubsection{Options' Test that They Are Loaded by \semantic}
+%
+% \label{page:testForSemanticsLoader}
+% The following does a test in all the options files to see whether they are
+% loaded from the \semantic\ package.  If not, no commands are defined.  See
+% also the bottom of the code part, where the mathcing "\fi" is provided.
+%    \begin{macrocode}
+%<*allOptions>
+\expandafter\ifx\csname sem@nticsLoader\endcsname\relax
+%    \end{macrocode}
+%  A feature of "\csname"\meta{name}"\endcsname" is that the command
+%  sequence would be taken to be "\relax" if \CSname{\meta{name}} is not
+%  defined.
+%    \begin{macrocode}
+  \PackageError{semantic}{%
+    This file should not be loaded directly}
+    {%
+      This file is an option of the semantic package.  It should not be
+        loaded directly\MessageBreak 
+      but by using \protect\usepackage{semantic} in your document 
+        preamble.\MessageBreak
+      No commands are defined.\MessageBreak
+     Type <return> to proceed.
+    }%
+\else
+%</allOptions>
+%    \end{macrocode}
+% This is the end of the part, which should not be processed when processing
+% the documentation
+%    \begin{macrocode}
+%<*documentation>
+\fi\fi
+%</documentation>
+%    \end{macrocode}
+%
+% \subsubsection{Auxiliary Macros}
+%
+%    \begin{macrocode}
+%<*general>
+\TestForConflict{\@dropnext,\@ifnext,\@ifn,\@ifNextMacro,\@ifnMacro}
+\TestForConflict{\@@maxwidth,\@@pLineBox,\if@@Nested,\@@cBox}
+\TestForConflict{\if@@moreLines,\@@pBox}
+%    \end{macrocode}
+%
+% \begin{macro}{\@ifnext}
+%   This macro compares the next token with a given token (\#1), and if they
+%   are identical, 
+%   the first choice (\#2) is expanded, else the second choice(\#3).
+%   This is a loan of "\@ifnextchar" from the \LaTeXe-base and it therefore
+%   uses the interal variables "\reserved@a"\lttdots"\reserved@d". The only
+%   change from "\@ifnextchar" is that spaces are not ignoree.  This is
+%  appropriate for defining 
+%   the ligatures (eg.\ I do not want \verb*"- >" to be converted to 
+%   $\rightarrow$).
+%    \begin{macrocode}
+\def\@ifnext#1#2#3{%
+  \let\reserved@e=#1\def\reserved@a{#2}\def\reserved@b{#3}\futurelet%
+  \reserved@c\@ifn} 
+\def\@ifn{%
+      \ifx \reserved@c \reserved@e\let\reserved@d\reserved@a\else%
+          \let\reserved@d\reserved@b\fi \reserved@d}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@ifNextMacro}
+%   This macro examines the next token, and if it is a macro, the first
+%   option (\#1) is executed, else the second option (\#2). Like
+%   "\@ifnext", the code is mainly ``borrowed'' from the \LaTeX-source.
+%    \begin{macrocode}
+\def\@ifNextMacro#1#2{%
+  \def\reserved@a{#1}\def\reserved@b{#2}%
+    \futurelet\reserved@c\@ifnMacro} 
+\def\@ifnMacro{%
+  \ifcat\noexpand\reserved@c\noexpand\@ifnMacro 
+    \let\reserved@d\reserved@a
+  \else \let\reserved@d\reserved@b\fi \reserved@d}
+%    \end{macrocode}
+%   The test of whether it is a macro, is done in "\@ifnMacro" by comparing the 
+%   catcodes of the token and a macro, "\@ifnMacro" (any other
+%   macro could have been used as well). The "\noexpand" secures that I compare 
+%   the token and not its expansion. If \emph{eg} "\@noexpand" were left out and 
+%   the token were a macro, then it would be expanded and the first token in 
+%   the macro be compared to the first token in "\@ifnMacro".
+% \end{macro}
+%
+% \begin{macro}{\@dropnext}
+%   This macro  processes the next token  and ignores its successor
+%   (it is not processed at all). 
+%    \begin{macrocode}
+\newcommand{\@dropnext}[2]{#1}
+%</general>
+%    \end{macrocode}
+%  \end{macro}
+%
+% \subsubsection{Testing for  Name Conflict  During Loading}
+%
+% At the end of the loading it is tested if an error has occurred.  In that
+% case an error message is issued.  Then the testing commands is disabled.
+%
+% \medskip\noindent But first  yet another documentation hack$\ldots$
+%    \begin{macrocode}
+%<*documentation>
+\iffalse
+%</documentation>
+%<*general>
+\ifnum \value{@@conflict} > 0
+   \PackageError{Semantic}
+     {The \the@@conflict\space command(s) listed above have been
+      redefined.\MessageBreak
+      Please report this to turtle@bu.edu}
+     {Some of the commands defined in semantic was already defined %
+      and has\MessageBreak now be redefined. There is a risk that %
+      these commands will be used\MessageBreak by other packages %
+      leading to spurious errors.\MessageBreak
+      \space\space Type <return> and cross your fingers%
+}\fi
+\let\@notdefinable=\@oldNotDefinable
+\let\@semanticNotDefinable=\relax
+\let\@oldNotDefinable=\relax
+\let\TestForConflict=\relax
+\let\@endmark=\relax
+\let\@test=\relax
+%</general>
+%    \end{macrocode}
+%
+% \medskip\noindent The end of yet another documentation hack
+%    \begin{macrocode}
+%<*documentation>
+\fi
+%</documentation>
+%    \end{macrocode}
+%
+% \subsection{Math Ligatures}
+%
+%    \begin{macrocode}
+%<*ligature>
+\TestForConflict{\@addligto,\@addligtofollowlist,\@def@ligstep}
+\TestForConflict{\@@trymathlig,\@defactive,\@defligstep}
+\TestForConflict{\@definemathlig,\@domathligfirsts,\@domathligfollows}
+\TestForConflict{\@exitmathlig,\@firstmathligs,\@ifactive,\@ifcharacter}
+\TestForConflict{\@ifinlist,\@lastvalidmathlig,\@mathliglink}
+\TestForConflict{\@mathligredefactive,\@mathligsoff,\@mathligson}
+\TestForConflict{\@seentoks,\@setupfirstligchar,\@try@mathlig}
+\TestForConflict{\@trymathlig,\if@mathligon,\mathlig,\mathligprotect}
+\TestForConflict{\mathligsoff,\mathligson,\@startmathlig,\@pushedtoks}
+%    \end{macrocode}
+%
+% \subsubsection{User Interface}
+% \label{sec:UserInterface}
+%
+% \begin{macro}{\if@mathligon}
+%   First we define a new "\if" flag that indicates whether the user has
+%   requested math ligatures to be active or not:
+%    \begin{macrocode}
+\newif\if@mathligon
+%    \end{macrocode}
+% \end{macro}
+% \begin{macro}{\mathlig}
+%   Now, for the definition of "\mathlig{"\meta{character
+%   sequence}"}{"\meta{ligature commands}"}", we first add the ligature
+%   character sequence $c_1c_2\cdots c_n$ to the internal ligature
+%   character lists, and then 
+%   we set up the macros "\@mathlig"$c_1c_2\cdots$ by calling
+%   "\@defligstep":
+%    \begin{macrocode}
+\DeclareRobustCommand\mathlig[1]{\@addligtolists#1\@@
+  \if@mathligon\mathligon\fi
+  \@setupfirstligchar#1\@@
+  \@defligstep{}#1\@@}
+%    \end{macrocode}
+%   \changes{2.0$\beta$}{2000/08/02}{Corrected typo in \CSname{mathligson}.}
+% \end{macro}
+% \DescribeMacro{\@mathligson}\DescribeMacro{\@mathligsoff}
+% We define macros "\@mathligson" and "\@mathligsoff" for turning math
+% ligatures on and off internally without changing the status of the
+% "\if@mathligon" flag:
+%    \begin{macrocode}
+\def\@mathligson{\if@mathligon\mathligson\fi}
+\def\@mathligsoff{\if@mathligon\mathligsoff\@mathligontrue\fi}
+%    \end{macrocode}
+% \begin{macro}{\mathligprotect}
+% "\mathligprotect{"\meta{command}"}" defines \meta{command} to be a macro
+% expanding into "\@mathligsoff"\emph{expansion
+% of}\meta{command}"\@mathligson":
+%    \begin{macrocode}
+\DeclareRobustCommand\mathligprotect[1]{\expandafter
+  \def\expandafter#1\expandafter{%
+    \expandafter\@mathligsoff#1\@mathligson}}
+%    \end{macrocode}
+% \end{macro}
+% \begin{macro}{\mathligson}
+% "\mathligson" changes the math code of all the characters that can occur
+% as the first character of a ligature character sequence to be active, and
+% sets the "\if@mathligon" flag:
+%    \begin{macrocode}
+\DeclareRobustCommand\mathligson{\def\do##1##2##3{\mathcode`##1="8000}%
+  \@domathligfirsts\@mathligontrue}
+%    \end{macrocode}
+%  and turn on math ligatures automatically.
+%    \begin{macrocode}
+\AtBeginDocument{\mathligson}
+%    \end{macrocode}
+%   \changes{2.0$\beta$}{2000/08/02}{Ligature turned on when ligatures are loaded (moved from \texttt{shorthand} option).}
+% \end{macro}
+% \begin{macro}{\mathligsoff}
+% "\mathligsoff" does the reverse actions: resetting math codes to their
+% values as recorded at ligature definition time (stored in the
+% "\@domathligfirsts" data structure).
+%    \begin{macrocode}
+\DeclareRobustCommand\mathligsoff{\def\do##1##2##3{\mathcode`##1=##2}%
+  \@domathligfirsts\@mathligonfalse}
+%    \end{macrocode}
+% \end{macro}
+%
+% \subsubsection{Utilities}
+% \label{sec:Utilities}
+%
+% \DescribeMacro{\@mathliglink} "\@mathliglink" is a dummy macro that
+% should never be expanded, so we issue an error if it is:
+%    \begin{macrocode}
+\edef\@mathliglink{Error: \noexpand\verb|\string\@mathliglink| expanded}
+%    \end{macrocode}
+% \DescribeMacro{\@ifcharacter}\DescribeMacro{\@ifactive}
+% "\@ifcharacter"\meta{character}"{"\meta{truebranch}"}{"\meta{falsebranch}"}" 
+% is used to test whether \meta{character} is in fact a character and chooses the
+% appropriate branch. "\@ifactive" is analogous.
+%    \begin{macrocode}
+{\catcode`\A=11\catcode`\1=12\catcode`\~=13 % Letter, Other and Active
+\gdef\@ifcharacter#1{\ifcat A\noexpand#1\let\next\@firstoftwo
+                \else\ifcat 1\noexpand#1\let\next\@firstoftwo
+                \else\ifcat \noexpand~\noexpand#1\let\next\@firstoftwo
+                \else\let\next\@secondoftwo\fi\fi\fi\next}%
+\gdef\@ifactive#1{\ifcat \noexpand~\noexpand#1\let\next\@firstoftwo
+                  \else\let\next\@secondoftwo\fi\next}}
+%    \end{macrocode}
+%
+% \subsubsection{Data Structures}
+% \label{sec:DataStructures}
+%
+% For each math ligature character sequence $c_1c_2\cdots c_n$ the macros
+% "\@mathlig"$c_1$, "\@mathlig"$c_1c_2$, \ldots, "\@mathlig"$c_1c_2\cdots
+% c_n$ are defined, and "\@mathlig"$c_1c_2\cdots c_n$ expands to the
+% commands that typeset the ligature. For $1<i<n$, if $c_1c_2\cdots c_i$ is
+% not also a ligature character sequence, it is defined as the (dummy)
+% macro "\@mathliglink"\DescribeMacro{\@mathliglink}.
+%
+% E.g.: if `"-><-"' has been defined to typeset as
+% "\rightarrow\leftarrow" and `"-->"' has been defined to typeset as
+% "\longrightarrow", the following macros will be defined:
+% \begin{center}
+% \begin{tabular}{ll}
+% \textbf{Macro} & \textbf{is defined as} \\
+% "\@mathlig-"     & "-"                     \\
+% "\@mathlig--"    & "\@mathliglink"         \\
+% "\@mathlig-->"   & "\longrightarrow"       \\
+% "\@mathlig->"    & "\@mathliglink"         \\
+% "\@mathlig-><"   & "\@mathliglink"         \\
+% "\@mathlig-><-"  & "\rightarrow\leftarrow" \\
+% \end{tabular}
+% \end{center}
+% As it can be seen, "\@mathlig"$c$ expands to $c$, so that the original
+% meaning of a single character $c$ can be used.
+%
+% The macro "\@domathligfirsts"\DescribeMacro{\@domathligfirsts} holds a
+% list of characters, which occur as a
+% first character in a ligature character sequence, with their 
+% "mathcode"s and "catcode"s as defined when the ligature is defined. E.g.:
+% if ligatures have been defined for `"-><-"' and `"<--"', then
+% "\@domathligfirsts" will expand into a token sequence containing the
+% sequence
+% \begin{center}
+% "\do \-{8704}{12}\do \<{12604}{12}"
+% \end{center}
+% Thus, defining command "\do#1#2#3{"\emph{manipulate character}"#1}" and
+% executing "\@domathligfirsts" manipulates all the first characters of
+% ligature character sequences.
+%
+% The macro "\@domathligfollows"\DescribeMacro{\@domathligfollows} is
+% analogous for characters that occur after the first character in a
+% ligature character sequence. "\@makemathligsactive" and
+% "\@makemathligsnormal" change the catcodes of these characters.
+%    \begin{macrocode}
+\def\@domathligfollows{}\def\@domathligfirsts{}
+\def\@makemathligsactive{\mathligson
+  \def\do##1##2##3{\catcode`##1=12}\@domathligfollows}
+\def\@makemathligsnormal{\mathligsoff
+  \def\do##1##2##3{\catcode`##1=##3}\@domathligfollows}
+%    \end{macrocode}
+% \begin{macro}{\@ifinlist}
+%   "\@ifinlist{"\meta{character/mathcode/catcode list}"}"\discretionary{}{}{}^^A
+%              "{"\meta{character}"}"\discretionary{}{}{}^^A
+%              "{"\meta{true\-branch}"}"\discretionary{}{}{}^^A
+%              "{"\meta{false\-branch}"}"
+%   checks whether \meta{character} is in \meta{character/mathcode/catcode
+%   list} and chooses the appropriate branch.
+%    \begin{macrocode}
+\def\@ifinlist#1#2{\@tempswafalse
+  \def\do##1##2##3{\ifnum`##1=`#2\relax\@tempswatrue\fi}#1%
+  \if@tempswa\let\next\@firstoftwo\else\let\next\@secondoftwo\fi\next}
+%    \end{macrocode}
+% \end{macro}
+%
+% \subsubsection{Setting up the Data Structures}
+% \label{sec:SettingUpTheDataStructures}
+%
+% \begin{macro}{\@addligto}
+% "\@addligto{"\meta{character/mathcode/catcode
+%   list}"}{"\meta{character}"}" inserts (replaces) or adds the "mathcode"
+%   and "catcode" information into the \meta{character/mathcode/catcode
+%   list}:
+%    \begin{macrocode}
+\def\@addligto#1#2{%
+  \@ifinlist#1#2{\def\do##1##2##3{\noexpand\do\noexpand##1%
+      \ifnum`##1=`#2 {\the\mathcode`#2}{\the\catcode`#2}%
+      \else{##2}{##3}\fi}%
+    \edef#1{#1}}%
+  {\def\do##1##2##3{\noexpand\do\noexpand##1%
+      \ifnum`##1=`#2 {\the\mathcode`#2}{\the\catcode`#2}%
+      \else{##2}{##3}\fi}%
+    \edef#1{#1\do#2{\the\mathcode`#2}{\the\catcode`#2}}}}
+%    \end{macrocode}
+% \end{macro}
+% \begin{macro}{\@addligtolists}
+% \begin{macro}{\@addligtofollowlist}
+% \errorcontextlines=10
+% "\@addligtolists{"\meta{$c_1c_2\cdots{}c_n$}"}" adds $c_1$ to the
+% "\@domathligfirsts" list and the remaining to the "\@domathligfollows"
+% list by only eating the first character and passing the remaining to
+% "\@addligtofollowlist":
+%    \begin{macrocode}
+\def\@addligtolists#1{\expandafter\@addligto
+  \expandafter\@domathligfirsts
+  \csname\string#1\endcsname\@addligtofollowlist}
+\def\@addligtofollowlist#1{\ifx#1\@@\let\next\relax\else
+  \def\next{\expandafter\@addligto
+    \expandafter\@domathligfollows
+    \csname\string#1\endcsname
+    \@addligtofollowlist}\fi\next}
+%    \end{macrocode}
+% \end{macro}
+% \end{macro}
+% \begin{macro}{\@defligstep}
+% \begin{macro}{\@def@ligstep}
+% "\@defligstep{"\meta{$c_1\cdots{}c_{i-1}$}"}{"\meta{$c_i$}"}" defines one
+% step in the parsing of a ligature character sequence: the
+% "\@mathlig"$c_1\cdots c_i$ macro. The (possibly active) characters are
+% turned into letters by applying "\string" until the end of the sequence
+% is reached:
+%    \begin{macrocode}
+\def\@defligstep#1#2{\def\@tempa##1{\ifx##1\endcsname
+    \expandafter\endcsname\else
+    \string##1\expandafter\@tempa\fi}%
+  \expandafter\@def@ligstep\csname @mathlig\@tempa#1#2\endcsname{#1#2}}
+%    \end{macrocode}
+% when the end of ALL the characters of the sequence (i.e.{} $c_1c_2\cdots
+% c_n$) is reached---signalled by the "\@@" control
+% sequence inserted by "\mathlig"---"\@def@ligstep" can define the macro
+% "\@mathlig"$c_1c_2\cdots
+% c_n$ (note that the following tokens in the input stream are the ones
+% following the first parameter of a "\mathlig" command). Otherwise, the
+% process is repeated by calling "\@defligstep" again.
+%    \begin{macrocode}
+\def\@def@ligstep#1#2#3{%
+  \ifx#3\@@
+    \def\next{\def#1}%
+  \else
+    \ifx#1\relax
+      \def\next{\let#1\@mathliglink\@defligstep{#2}#3}%
+    \else
+      \def\next{\@defligstep{#2}#3}%
+    \fi
+  \fi\next}
+%    \end{macrocode}
+% \end{macro}
+% \end{macro}
+% \begin{macro}{\@setupfirstligchar}
+% The first character, $c$, of a ligature sequence must receive special
+% treatment: if it is already active, we must redefine it to check whether
+% it is used inside or outside of math. When inside, it should expand to
+% "\@startmathlig"$c$\SpecialUsageIndex{\@startmathlig}.
+%    \begin{macrocode}
+\def\@setupfirstligchar#1#2\@@{%
+  \@ifactive{#1}{%
+    \expandafter\expandafter\expandafter\@mathligredefactive
+    \expandafter\string\expandafter#1\expandafter{#1}{#1}}%
+%    \end{macrocode}
+% If on the other hand it is not active, we must define \emph{its active
+% variant} to expand to "\@startmathlig"$c$. This cannot be done directly,
+% as we cannot change the "catcode"s of characters once they've been read,
+% so we call "\@defactive":
+%    \begin{macrocode}
+  {\@defactive#1{\@startmathlig #1}\@namedef{@mathlig#1}{#1}}}
+%    \end{macrocode}
+% \end{macro}
+% \begin{macro}{\@mathligredefactive}
+% The use of "\@mathligredefactive" is tricky: the macro needs three
+% versions of the character to be defined: an active (for defining), a
+% letter (for "\@namedef"ining) and an expanded version (for wrapping the
+% math mode check stuff around). thus it must be called by
+% "\@mathligredefactive{"\meta{letter}"}{"\meta{expansion}"}{"\meta{active
+% character}"}".
+%    \begin{macrocode}
+\def\@mathligredefactive#1#2#3{%
+  \def#3{{}\ifmmode\def\next{\@startmathlig#1}\else
+    \def\next{#2}\fi\next}%
+  \@namedef{@mathlig#1}{#2}}
+%    \end{macrocode}
+% \end{macro}
+% \begin{macro}{\@defactive}
+% \begin{macro}{\@definemathlig}
+% The only way we can get an active version of a character $c$ is by
+% storing a list of possible characters, each with catcode 13
+% (active). Actually, what we do is to have a list of macros,
+% "\@definemathlig"$c$"{"\meta{expansion text}"}" that will define the
+% active character $c$ to expand to \meta{expansion text}.
+%    \begin{macrocode}
+\def\@defactive#1{\@ifundefined{@definemathlig\string#1}%
+  {\@latex@error{Illegal first character in math ligature}
+    {You can only use \@firstmathligs\space as the first^^J
+      character of a math ligature}}%
+  {\csname @definemathlig\string#1\endcsname}}
+
+{\def\@firstmathligs{}\def\do#1{\catcode`#1=\active
+    \expandafter\gdef\expandafter\@firstmathligs
+    \expandafter{\@firstmathligs\space\string#1}\next}
+  \def\next#1{\expandafter\gdef\csname
+    @definemathlig\string#1\endcsname{\def#1}}
+%    \end{macrocode}
+% Well, this is the list of characters I found it reasonable to expect as
+% first characters of a ligature sequence. Characters like "$" "&" "^" "_"
+% "#" "\" and "%" don't really make sense. All these characters are put
+% into a comma separated list,
+% "\@firstmathligs"\DescribeMacro{\@firstmathligs}.
+%    \begin{macrocode}
+  \do{"}"\do{@}@\do{/}/\do{(}(\do{)})\do{[}[\do{]}]\do{=}=
+  \do{?}?\do{!}!\do{`}`\do{'}'\do{|}|\do{~}~\do{<}<\do{>}>
+  \do{+}+\do{-}-\do{*}*\do{.}.\do{,},\do{:}:\do{;};}
+%    \end{macrocode}
+% \end{macro}
+% \end{macro}
+%
+% \subsubsection{Parser Algorithm}
+% \label{sec:ParserAlgorithm}
+%
+% During parsing, 
+% \begin{itemize}
+%   \item \DescribeMacro{\@seentoks}"\@seentoks" holds the characters seen
+%     so far. 
+%   \item \DescribeMacro{\@lastvalidmathlig}"\@lastvalidmathlig" holds the
+%     macro corresponding to the longest 
+%     valid math ligature character sequence seen so far
+%   \item \DescribeMacro{\@pushedtoks}"\@pushedtoks" holds the remaining
+%     characters seen that are not a 
+%     part of the valid ligature character sequence
+% \end{itemize}
+%    \begin{macrocode}
+\newtoks\@pushedtoks
+\newtoks\@seentoks
+%    \end{macrocode}
+%
+% The overall algorithm is as follows:
+%
+% \begin{itemize}
+%   \item [1] Let $i=1$. A character $c_i$ in "\@domathligfirsts" triggers
+%     the following steps:
+%   \item [2] 
+%        \begin{tabbing}
+%        "\@seentoks" := [ ] \\
+%        "\@lastvalidmathlig" := \{\} \\
+%        "\@pushedtoks" := [ ]
+%        \end{tabbing}
+%   \item [3]
+%     \begin{tabbing}\qquad\=\qquad\=\qquad\=\kill
+%        if the macro "\@mathlig"$c_1c_2\cdots c_i$ is defined then \\
+%          \>if "\@mathlig"$c_1c_2\cdots c_i$ is a "\@mathliglink" then \\
+%            \>\>"\@pushedtoks" := "\@pushedtoks" ++ [$c_i$] \\
+%          \>else \\
+%            \>\>"\@lastvalidmathlig" := "\@mathlig"$c_1c_2\cdots c_i$ \\
+%            \>\>"\@pushedtoks" := [ ] \\
+%          \>"\@seentoks" := "\@seentoks" ++ [$c_i$] \\
+%        else \\
+%          \>disable ligatures \\
+%          \>expand "\@lastvalidmathlig" \\
+%          \>enable ligatures \\
+%          \>put the "\@pushedtoks" and $c_i$ on the input stream \\
+%          \>go to 1
+%     \end{tabbing}
+%   \item [4] Let $i=i+1$; read next character $c_i$ and go to 3.
+% \end{itemize}
+% \begin{macro}{\@startmathlig}
+% \begin{macro}{\@trymathlig}
+% \begin{macro}{\@@trymathlig}
+% \begin{macro}{\@try@mathlig}
+% \begin{macro}{\@exitmathlig}
+% All this is accomplished by the following macros, starting with
+% "\@startmathlig": 
+%    \begin{macrocode}
+\def\@startmathlig{\def\@lastvalidmathlig{}\@pushedtoks{}%
+  \@seentoks{}\@trymathlig}
+\def\@trymathlig{\futurelet\next\@@trymathlig}
+\def\@@trymathlig{\@ifcharacter\next{\@try@mathlig}{\@exitmathlig{}}}
+\def\@exitmathlig#1{%
+  \expandafter\@makemathligsnormal\@lastvalidmathlig\mathligson
+  \the\@pushedtoks#1}
+\def\@try@mathlig#1{%\typeout{char: #1 catcode: \the\catcode`#1
+%^^A    \space pushed:\the\@pushedtoks
+%^^A    \space seen:\the\@seentoks
+%^^A    \space last\meaning\@lastvalidmathlig}%
+  \@ifundefined{@mathlig\the\@seentoks#1}{\@exitmathlig{#1}}%
+  {\expandafter\ifx
+         	 \csname @mathlig\the\@seentoks#1\endcsname
+         	 \@mathliglink
+      \expandafter\@pushedtoks
+        \expandafter=\expandafter{\the\@pushedtoks#1}%
+    \else
+      \expandafter\let\expandafter\@lastvalidmathlig
+      \csname @mathlig\the\@seentoks#1\endcsname
+      \@pushedtoks={}%
+    \fi
+    \expandafter\@seentoks\expandafter=\expandafter%
+    {\the\@seentoks#1}\@makemathligsactive\obeyspaces\@trymathlig}}
+%    \end{macrocode}
+% \end{macro}
+% \end{macro}
+% \end{macro}
+% \end{macro}
+% \end{macro}
+%
+% \subsubsection{Compatibility with \texttt{amsmath} package}
+%
+% \begin{macro}{\patch@newmcodes@}
+%   The \texttt{amsmath} package by AMS uses some non-alphanumeric
+%   characters to produce for instance extended arrows.  Consequently
+%   the  "\newmcodes@" in \texttt{amsopn.sty} (2.01) fails with an error message if
+%   the hyphen character has mathcode \"8000. So we in provide a patch
+%   (suggested by Michael John Downes of AMS<). 
+%    \begin{macrocode}
+\edef\patch@newmcodes@{%
+  \mathcode\number`\'=39
+  \mathcode\number`\*=42
+  \mathcode\number`\.=\string "613A
+  \mathchardef\noexpand\std@minus=\the\mathcode`\-\relax
+  \mathcode\number`\-=45
+  \mathcode\number`\/=47
+  \mathcode\number`\:=\string "603A\relax
+}
+\AtBeginDocument{\let\newmcodes@=\patch@newmcodes@}
+%</ligature>
+%    \end{macrocode}
+% \changes{2.0$\gamma$}{2002/06/13}{Provided patch to make \semantic compatible with \texttt{amsmath} v. 2.01}
+% \end{macro}
+%
+% \subsubsection{ToDo}
+% \label{sec:ToDo}
+% 
+% \begin{itemize}
+% \item Make removing of math ligatures possible (tricky!)
+% \item Make it possible to define a single char as a ligature
+%       (redefinition)
+% \item Check the use of "\@makemathligsactive": is it possible to
+%       replace it by "\mathligson"?
+% \end{itemize}
+%
+% \subsection{Inference Rules}
+%
+%    \begin{macrocode}
+%<*inference>
+\TestForConflict{\@@tempa,\@@tempb,\@adjustPremises,\@inference}
+\TestForConflict{\@inferenceBack,\@inferenceFront,\@inferenceOrPremis}
+\TestForConflict{\@premises,\@processInference,\@processPremiseLine}
+\TestForConflict{\@setLengths,\inference,\predicate,\predicatebegin}
+\TestForConflict{\predicateend,\setnamespace,\setpremisesend}
+\TestForConflict{\setpremisesspace,\@makeLength,\@@space}
+\TestForConflict{\@@aLineBox,\if@@shortDivider}
+%    \end{macrocode}
+% \begin{macro}{\@makeLength}
+%   \changes{1.1}{1995/11/12}{Redefined the lengths commands, so that the lengths are evaluated each time}^^A
+% \begin{macro}{\@setLengths}
+% \changes{1.1$\beta$}{1995/11/21}{Added setting of parameters for line skipping in \CSname{@setLengths}}
+%   First I define two auxiliary macros to facilitate the use of the lengths
+%   controlling the appearance of an inference rule.  My overall aim is to
+%   allow the use of relative units ("em" and "ex"). To accomplish this, the
+%   lengths have to be evaluated before the setting of every rule. As
+%   there are only a few lengths, it could been have been simpler and less
+%   general, but I found it inspiring to work out a general solution.
+%
+%   "\@makelength{"\meta{users name}"}{"\meta{internal name}"}{"\meta{default
+%       value}"}{"\meta{stretch}"}" does all the definitions associated with
+%   making a new length: defines a new length "\@@"\meta{internal name}, makes
+%   a command to evaluate it (with the current choice of font)
+%   "\@set"\meta{internal name} and makes the users command to change the
+%   length "\set"\meta{users name}.  \meta{default value} is---of course---the
+%   normal value used for the length, while \meta{stretch} is the stretch
+%   parameter in case the premise should be set wider than its natural width.
+%
+%   The macro "\@setLengths" is used to evaluate all the lengths. When a new
+%   length is made using "\@makelength", the name of its evaluation macro,
+%   "\@set"\meta{internal name}, is added. 
+%    \begin{macrocode}
+\newtoks\@@tempa 
+\newtoks\@@tempb 
+\newcommand{\@makeLength}[4]{
+  \@@tempa=\expandafter{\csname @@#2\endcsname}
+  \@@tempb=\expandafter{\csname @set#2\endcsname} %
+  \expandafter \newlength \the\@@tempa 
+  \expandafter \newcommand \the\@@tempb {} 
+  \expandafter \newcommand \csname set#1\endcsname[1]{}
+  \expandafter \xdef \csname set#1\endcsname##1%
+    {{\dimen0=##1}%
+      \noexpand\renewcommand{\the\@@tempb}{%
+        \noexpand\setlength{\the \@@tempa}{##1 #4}}%
+    }%
+  \csname set#1\endcsname{#3}
+  \@@tempa=\expandafter{\@setLengths} %
+  \edef\@setLengths{\the\@@tempa \the\@@tempb} %
+  }
+
+\newcommand{\@setLengths}{%
+  \setlength{\baselineskip}{1.166em}%
+  \setlength{\lineskip}{1pt}%
+  \setlength{\lineskiplimit}{1pt}}
+%    \end{macrocode}
+%   The first lines in "\@makelength" builds the name of the length in
+%   "\@@tempa" and the macro to evaluate it in "\@@tempb"---this requires some
+%   playing with "\csname"---and declares the corresponding length and command.
+%   Then the users command is builded: It contains a test "{\dimen0 = #1}" to
+%   ensure that the given parameter  is, in fact, a length and then it
+%   redefines the evaluating command so that the length is the length
+%   provided by the user, and a possibly stretch which is defined below and
+%   cannot be altered by the user. At last the evaluating command is added to
+%   "\@setLengths"---the inspiration to this code I got from
+%   \cite[378]{texbook}.
+%
+%   The distance between the lines of premises is set by \TeX\ using its normal
+%   lineskipping algorithm. As some environments, e.g.\ "tabular", sets all the
+%   lineskipping  parameters, "\baselineskip", "\lineskip" and 
+%   "\lineskiplimit", to zero it is necessary to set them in "\@setLengths".
+% \end{macro}
+% \end{macro}
+%
+% \begin{macro}{\setpremisesspace}
+%   \changes{1.0}{1995/10/18}{Changed from 10"pt" to 15"pt"}^^A
+%   \changes{1.2$\alpha$}{1996/01/31}{Changed to 1.5"em"}
+% \begin{macro}{\setpremisesend}
+%   \changes{1.2$\alpha$}{1996/01/31}{Changed to .75"em"}
+% \begin{macro}{\setnamespace}
+%   \changes{1.01}{1995/11/07}{Introduced \CSname{name\-space}}^^A
+%   This is followed by the definition of some auxiliary internal registers:
+%   \label{space setting}
+%    \begin{macrocode}
+\@makeLength{premisesspace}{pSpace}{1.5em}{plus 1fil}
+\@makeLength{premisesend}{pEnd}{.75em}{plus 0.5fil}
+\@makeLength{namespace}{nSpace}{.5em}{}
+%</inference>
+%    \end{macrocode}
+% \end{macro}
+% \end{macro}
+% \end{macro}
+%
+% Then comes some auxiliary internal registers
+% \changes{1.1$\delta$}{1995/12/01}{Introduced \CSname{@@space} for use in comparisons}
+%    \begin{macrocode}
+%<*general>
+\newdimen\@@maxwidth 
+\newbox\@@pLineBox
+\newbox\@@cBox 
+\newbox\@@pBox 
+\newif\if@@moreLines
+%</general>
+%<*inference>
+\newbox\@@aLineBox 
+\newif\if@@shortDivider
+\newcommand{\@@space}{ }
+%    \end{macrocode}
+% \begin{tabular}{lp{9.4cm}}
+%   "\@@maxwidth" & The largest width of a premise/ \\
+%   "\@@cBox" & Holds the conclusion when it has been built \\
+%   "\@@pBox" & The premises is built in this register  \\
+%   "\@@pLineBox" & Used to build a single line of the premise \\
+%   "\@@aLineBox" & Contains the line to be adjusted  \\
+%   "\@@moreLines" & Flag telling if there is more lines of premises to process \\
+%   "\@@moreLines" & Flag telling the divider should only be the length of
+%   the conclusion \\
+%   "\@@space" & Macro with a single space---used for comparison.
+% \end{tabular}
+%
+% \begin{macro}{\predicate}
+% \begin{macro}{\predicatebegin}
+% \changes{1.0}{1995/10/18}{Changed the name to avoid conflict with \LaTeX}
+% \changes{2.0}{1998/06/05}{Changed the default setting to "$" such that
+% the premises are set in math mode.}
+% \begin{macro}{\predicateend}
+% \changes{1.0}{1995/10/18}{Changed the name to avoid conflict with \LaTeX}
+% \changes{2.0}{1998/06/05}{Changed the default setting to "$" such that
+% the premises are set in math mode.}
+%   "\predicate" controls the setting of a single predicate cf.\ 
+%   p.~\pageref{pattern matching}.
+%    \begin{macrocode}
+\newcommand{\predicate}[1]{\predicatebegin #1\predicateend}
+\newcommand{\predicatebegin}{$}
+\newcommand{\predicateend}{$}
+%    \end{macrocode}
+% \end{macro}
+% \end{macro}
+% \end{macro}
+%
+% \subsection{Typesetting Inference Rules}
+%
+%   These macros typesets inference rules.  The macros are used nested,
+%   which means that \TeX{}'s stack is used extensively.  In
+%   particular, these put a heavy burden on the paramter stack. To
+%   circumvent this the macros are splitted such that each macro only 
+%   parses one argument at a time.  Then only the arguments
+%   containing the premise are saved.   It is still worth considering 
+%   ways to remove more nesting of macros with arguments, for
+%   instance one could probaply test if the following token was a
+%   begin group and then redefine the meaning of~"&" and~"\\".  The
+%   drawback is that it then might be necessary to use active
+%   characters.
+%
+% \begin{macro}{\inference}
+% \changes{1.0}{1995/18/10}{Changed some names due to a conflict with \LaTeX's \CSname{rule}}
+% \changes{1.01}{1995/11/07}{Inserted a space in front of the name using \CSname{name\-space}}
+% \changes{1.1}{1995/11/15}{Removed \CSname{@pInference}}
+% \changes{2.0}{1998/05/20}{Added check for starred version}
+%  This is the entry macro.  It starts the parameter parsig by testing 
+%  for the starred version; this is stored in the value of
+%  "\if@@shortDivider".  It starts a group that the full inference
+%  with names is saved in.
+%    \begin{macrocode}
+\def\inference{%
+  \@@shortDividerfalse
+  \expandafter\hbox\bgroup
+  \@ifstar{\@@shortDividertrue\@inferenceFront}%
+          \@inferenceFront
+}
+%    \end{macrocode}
+% \end{macro}
+% 
+% \begin{macro}{\@inferenceFront}
+%   This macro testes for an optional argument to the left of the
+%   inference. 
+%    \begin{macrocode}
+\def\@inferenceFront{%
+  \@ifnextchar[%
+     {\@inferenceFrontName}%
+     {\@inferenceMiddle}%
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@inferenceFrontName}
+%   This maacro typesets an optional argument with the apropriate
+%   space and then passes control to the typesetting of the inference
+%    \begin{macrocode}
+\def\@inferenceFrontName[#1]{%
+  \setbox3=\hbox{\footnotesize #1}%
+  \ifdim \wd3 > \z@
+    \unhbox3%
+    \hskip\@@nSpace
+  \fi
+  \@inferenceMiddle
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@inferenceMiddle}
+%   It typesets the premises in the box~"\@@pBox".
+%    \begin{macrocode}
+\long\def\@inferenceMiddle#1{%
+  \@setLengths%
+%    \end{macrocode}
+%   Initialises the length parameters according to the current font
+%   size.
+%    \begin{macrocode}
+  \setbox\@@pBox=
+    \vbox{%
+      \@premises{#1}%
+      \unvbox\@@pBox
+    }%
+%    \end{macrocode}
+%   This typesets the premises.  It is necessary to have the
+%   typesetting in its own group to prevent interferring with a
+%   premise being typeset on the outer levels.  We therefore typeset
+%   the premises inside a group and moves them one level out by
+%   "\unvbox" inside a~"\vbox".
+%    \begin{macrocode}
+  \@inferenceBack
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@inferenceBack}
+%  This macro typesets the conclusion, sets up the premises on top of
+%  the conclusion and tests for an additional argument.
+%    \begin{macrocode}
+\long\def\@inferenceBack#1{%
+  \setbox\@@cBox=%
+   \hbox{\hskip\@@pEnd \predicate{\ignorespaces#1}\unskip\hskip\@@pEnd}%
+%    \end{macrocode}
+%  Typeset the conclusion in its own box.  In this way we are able to
+%  compare the lengths of the two.
+%    \begin{macrocode}
+  \setbox1=\hbox{$ $}%
+%    \end{macrocode}
+%  We then ensure that we have the right math fonts loaded by changing 
+%  to math mode.
+%    \begin{macrocode}
+  \setbox\@@pBox=\vtop{\unvbox\@@pBox
+      		 \vskip 4\fontdimen8\textfont3}%
+  \setbox\@@cBox=\vbox{\vskip 4\fontdimen8\textfont3%
+      		 \box\@@cBox}%
+%    \end{macrocode}
+%  Add the space corresponding to a fraction bar in a display below
+%  the premises and above the conclusion.  
+%    \begin{macrocode}
+  \if@@shortDivider
+%    \end{macrocode}
+%  If the user want a short divider, we typeset the premises and the
+%  conclusion in a box with the width of the biggest of the two, but
+%  ensures that the divider only gets the width of the
+%  conclusion. Anyway, this is not really what we want.  We should
+%  somehow know the length of the previous premise, but I have not
+%  worked out the algorithm yet.
+%    \begin{macrocode}
+    \ifdim\wd\@@pBox >\wd\@@cBox%
+      \dimen1=\wd\@@pBox%
+    \else%
+      \dimen1=\wd\@@cBox%
+    \fi%
+    \dimen0=\wd\@@cBox%
+    \hbox to \dimen1{%
+      \hss
+      $\frac{\hbox to \dimen0{\hss\box\@@pBox\hss}}%
+        {\box\@@cBox}$%
+      \hss
+    }%
+  \else
+%    \end{macrocode}
+%   If plain style, we simply typeset the premise on top of the
+%   conclusion. 
+%    \begin{macrocode}
+    $\frac{\box\@@pBox}%
+          {\box\@@cBox}$%
+  \fi
+  \@ifnextchar[%
+     {\@inferenceBackName}%{}%
+     {\egroup}
+}
+%    \end{macrocode}
+%  We end the typesetting by testing for an optional argument.  If
+%  this is not provided we simply ends the group started by
+%  "\inference". 
+% \end{macro}
+%
+% \begin{macro}{\@inferenceBackName}
+%   Here we typeset an additional argument
+%    \begin{macrocode}
+\def\@inferenceBackName[#1]{%
+  \setbox3=\hbox{\footnotesize #1}%
+  \ifdim \wd3 > \z@
+    \hskip\@@nSpace
+    \unhbox3%
+  \fi
+%    \end{macrocode}
+% and end the group started by "\inference".
+%    \begin{macrocode}
+  \egroup
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \subsubsection{Processing of Premises}
+%
+% Then comes the code that processes a list of premises and set them in
+% "\@@pBox". I do a lot of gambots adding and deleting extra tokens so that
+% \TeX's pattern mathcing on macro arguments can be used to find nestings,
+% linebreaks etc.\ as I belive this to be faster than actually reading 
+% one token at a time using \TeX\ primitives.
+%
+% \begin{macro}{\@premises}
+%   \changes{1.1}{1995/11/25}{Initially set \CSname{@max\-width} equal to the width of the conclusion}
+% \changes{1.1$\gamma$}{1995/11/12}{Changed \CSname{@premises} so the
+% premises can extend over several lines}
+%   This initialises the processing of the list of premises line by line. A
+%   line is recognised in "\@processPremises", which does the processing by
+%   matching on its terminating "\\". Since there is not a "\\" after the last
+%   premise, I insert \verb*"\\ \end" as an end marker after the list of
+%   premises. In this way, "\@processPremises" can assume that every line is
+%   followed by "\\", and if this is followed by "\end", it has reached the
+%   end.
+%    \begin{macrocode}
+\newcommand{\@premises}[1]{%
+  \setbox\@@pBox=\vbox{}%
+  \dimen\@@maxwidth=\wd\@@cBox%
+  \@processPremises #1\\\end%
+  \@adjustPremises%
+}
+%    \end{macrocode}
+%   In cases where there---as an example---are two narrow premises on one line
+%   and a broad one on another line. it would look strange if the distance between
+%   the two premises were fixed. I therefore add som strechable glue
+%   between the premises and at the end (with half the strechability) 
+%   cf.~p.~\pageref{space setting}. To accomplish this, I need to know the 
+%   width of the widest line, but this can only be found while processing
+%   the premises. It is saved in "\@@maxwidth" so that "\@adjustPremises" adjusts
+%   all lines to it. By initially setting "\@@maxwidth" to the width of the
+%   conclusion, no line will become narrower than the conclusion. And due to the
+%   glue, the premises will appear centered if the conclusion is wider than the
+%   premises.
+% \end{macro}
+%
+% \begin{macro}{\@adjustPremises}
+%   This macro adjusts  the lines of premises to "\@@maxwidth":
+%    \begin{macrocode}
+\newcommand{\@adjustPremises}{%
+  \setbox\@@pBox=\vbox{%
+    \@@moreLinestrue %
+    \loop %
+      \setbox\@@pBox=\vbox{%
+        \unvbox\@@pBox %
+        \global\setbox\@@aLineBox=\lastbox %
+      }%
+      \ifvoid\@@aLineBox %
+        \@@moreLinesfalse %
+      \else %
+        \hbox to \dimen\@@maxwidth{\unhbox\@@aLineBox}%
+      \fi % 
+    \if@@moreLines\repeat%
+  }%
+}
+%    \end{macrocode}
+%   The lines set are put in "\@@pBox" in reverse order. They are taken from
+%   "\@@pBox" one by one by emptying ("\unvbox") "\@@pBox", setting
+%   "\@@aLineBox" to the last box in the vertical list just emptied and putting
+%   the rest back in "\@@pBox". I do not expect this to be as bas as it sounds,
+%   because presumably the "\unvbox" is not a actual copying but only some
+%   pointer operation, which can be done in constant time (cf.\ the hints on
+%   \cite[120]{texbook}).
+%   
+%   All this is done inside a "\vbox" so the contents of "\@@aLineBox" can be
+%   added to the list being build simply using "\hbox to "\lttdots\ (doing the
+%   adjusting simultaneousnessly). Being inside a "\vbox" has the additional
+%   advantage that \TeX\ is in internal vertical mode so that there
+%   is added lineskip automaticly in accordance with "\baselineskip" etc.\ 
+%   (cf.~\cite[80]{texbook}). As the macro is in no sense recursive, it is no
+%   problem changing "\@aLineBox"  globally.
+% \end{macro}
+% 
+% \begin{macro}{\@processPremises}\mbox{}^^A
+% \changes{1.1$\beta$}{1995/11/21}{Fixed bug that made an empty premise sometimes contain \CSname{pSpace}}
+% \changes{1.1$\beta$}{1995/11/21}{Moved the processing of spaces to \CSname{@inferenceOrPremis}}
+%    \begin{macrocode}
+\def\@processPremises#1\\#2\end{%
+%    \end{macrocode}
+%   This pattern splits the list of premises into the first
+%   line (\#1---possibly empty) and the following lines
+%   (\#2---possibly containing no lines).   
+%    \begin{macrocode}
+  \setbox\@@pLineBox=\hbox{}%
+  \@processPremiseLine #1&\end%
+  \setbox\@@pLineBox=\hbox{\unhbox\@@pLineBox \unskip}% 
+%    \end{macrocode}
+%   The first line is typesetted in "\@@pLineBox" and additional space 
+%   is removed.  We use "\@processPremiseLine" that like
+%   "\@processPremises" gets "&\end" added so that it recognizes the
+%   end of line. After the line has been set   
+%    \begin{macrocode}
+  \ifdim \wd\@@pLineBox > \z@ %
+%    \end{macrocode}
+%   If the premise is not empty, we add it to "\@@pBox", that when finished
+%   will contain the lines (in reverse order---cf.~"\@adjustPremises"), and if
+%   necessary "\@@maxwidth" is increased. 
+%    \begin{macrocode}
+    \setbox\@@pLineBox=%
+      \hbox{\hskip\@@pEnd \unhbox\@@pLineBox \hskip\@@pEnd}%
+    \ifdim \wd\@@pLineBox > \dimen\@@maxwidth %
+      \dimen\@@maxwidth=\wd\@@pLineBox %
+    \fi %
+    \setbox\@@pBox=\vbox{\box\@@pLineBox\unvbox\@@pBox}%
+  \fi %
+%    \end{macrocode}
+%  If there are more line we process them.
+%    \begin{macrocode}
+  \def\@temp{#2}%
+  \ifx \@temp\empty \else %
+    \@ReturnAfterFi{%
+      \@processPremises #2\end %
+    }%
+%    \end{macrocode}
+%  "\@ReturnAfterFi" is a trick due to Heiko Oberdik to ensure that we 
+%  get a tail recursive macro.
+%    \begin{macrocode}
+  \fi%
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@processPremiseLine}\mbox{}^^A
+% \changes{1.1$\delta$}{1995/12/01}{Fixed bug that axioms could not be handled using pattern matching}
+%    \begin{macrocode}
+\def\@processPremiseLine#1&#2\end{%
+%    \end{macrocode}
+%   This pattern splits the line into the first premise (\#1---possibly
+%   empty) and the following premises (\#2---possibly none). 
+%    \begin{macrocode}
+  \def\@temp{#1}%
+  \ifx \@temp\empty \else%
+    \ifx \@temp\@@space \else%
+    \setbox\@@pLineBox=%
+      \hbox{\unhbox\@@pLineBox%
+            \@inferenceOrPremis #1\inference\end%
+            \hskip\@@pSpace}%
+    \fi%
+  \fi%
+%    \end{macrocode}
+%   If the first premise is non-empty, which in this context means that
+%   it is neither empty nor a space (\verb*+& &+ should be regarded as an 
+%   empty premise), it is typesetted using
+%   "\@inferenceOrPremis", and an appropriate spacing to the next premise is
+%   added. Note that this space is also added after the last premise but then
+%   removed again, when \LaTeX\ has returned to "\@processPremises".
+%    \begin{macrocode}
+  \def\@temp{#2}%
+  \ifx \@temp\empty \else%
+    \@ReturnAfterFi{%
+      \@processPremiseLine#2\end%
+    }%
+  \fi%
+}
+%    \end{macrocode}
+%  If there are any premises in the
+%   \emph{following premises} we use "\@processPremisesLine" 
+%   tail recursively.
+% \end{macro}
+%
+% \begin{macro}{\@inferenceOrPremis}
+%   "@inferenceOrPremis" decides wether there is a nested "\@inference" in a
+%   premise. 
+%    \begin{macrocode}
+\def\@inferenceOrPremis#1\inference{%
+  \@ifnext \end 
+    {\@dropnext{\predicate{\ignorespaces #1}\unskip}}%
+    {\@processInference #1\inference}%
+}
+%    \end{macrocode}
+%   The calling macro appends the argument with "\inference \end". We
+%   then test whether "\inference" followd by the token~"\end".  If
+%   this is the case, we conclude that premise did not originally 
+%   contain a nesting (\emph{ie} "\inference"). In this case, 
+%   the "\end"-token is removed and the premise is set using
+%   "\predicate". Otherwise, "\inference"
+%   "\end" is removed and the inference rule is set---all this is done by
+%   "\@processInference".
+% \end{macro}
+%
+% \begin{macro}{\@processInference}
+%   Remove "\inference" "\end" from the testing for a nested
+%   appearance of an inference rule.  Typesets the inference and
+%   adjust its vertical placement  such that the baseline of its
+%   conclusion match the baseline of a plain premise.
+%    \begin{macrocode}
+\def\@processInference#1\inference\end{%
+  \ignorespaces #1%
+%    \end{macrocode}
+%  Typesets the inference rule and returns the full inference rule in
+%  a box.
+%    \begin{macrocode}
+  \setbox3=\lastbox
+  \dimen3=\dp3
+  \advance\dimen3 by -\fontdimen22\textfont2
+  \advance\dimen3 by \fontdimen8\textfont3
+  \expandafter\raise\dimen3\box3%  
+%    \end{macrocode}
+%  We take the previously type setted inference rule and lifts it by
+%  its depth modulo the extra depth that it has got from be lowered
+%  by a fraction.
+%    \begin{macrocode}
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@ReturnAfterFi}
+%   This is a small macro due to Heiko Oberdik.  It ensure that we get 
+%   a tail recursive function even inside an "\if"-construction.
+%    \begin{macrocode}
+\long\def\@ReturnAfterFi#1\fi{\fi#1}
+%    \end{macrocode}
+%  It finds the commands up till the enclosing "\fi", closes the "\if" 
+%  and executes the commands.
+% \end{macro}
+%
+%    \begin{macrocode}
+%</inference>
+%    \end{macrocode}
+%
+% \subsubsection{ToDo}
+% 
+% \begin{itemize}
+% \item Find a way to made the conclusion bar as wide as the
+%       conclusion of the premises (tricky).
+% \item Get it to work correctly with amsmath and mathbbol
+% \end{itemize}
+%
+% \subsection{T-diagrams}
+%
+%    \begin{macrocode}
+%<*Tdiagram>
+\TestForConflict{\@getSymbol,\@interpreter,\@parseArg,\@program}
+\TestForConflict{\@putSymbol,\@saveBeforeSymbolMacro,\compiler}
+\TestForConflict{\interpreter,\machine,\program,\@compiler}
+%</Tdiagram>
+%    \end{macrocode}
+% First some auxilary registers are reserved:
+%    \begin{macrocode}
+%<*general>
+\newif\if@@Nested \@@Nestedfalse 
+%</general>
+%<*Tdiagram>
+\newif\if@@Left 
+\newif\if@@Up
+\newcount\@@xShift 
+\newcount\@@yShift 
+\newtoks\@@symbol
+\newtoks\@@tempSymbol
+%    \end{macrocode}
+% \begin{tabular}{lp{9.2cm}}
+%   "\@@Nested" & Flag telling if the current diagram is nested within another \\
+%   "\@@Left"   & Flag telling that a nested diagram should be drawn to the
+%                 left---if not set, the nested diagram is drawn to the right \\
+%   "\@@Right"  & Flag telling that a nested diagram should be drawn above 
+%                 the current one---if not set, the diagram is drawn below
+%                 the current one \\
+%   "\@@xShift" & Horizontal shift from the local origin to the starting
+%                 position in units of "\unitlength". \\
+%   "\@@yShift" & Vertical shift from the local origin to the starting
+%                 position in units of "\unitlength" \\
+%   "\@@Symbol" & The current machine symbol (i.e.\ the letter designating
+%                 the programme/machine) \\
+%   "\@@tempSymbol" & Used as temporary storage for different symbols 
+% \end{tabular}
+% 
+% When \LaTeX's "\put" command is invoked, it raises a "\hbox" to
+% the given offset, giving it height zero, and puts a "\hss" in the end
+% so that it will end up with zero width too. It expands the "picture" command
+% given in "{"\lttdots"}" just before the "\hss", so they can be drawn
+% from a local origin (given as coordinates to "\put"). The
+% diagram commands are adapted to this scheme. Thus they are all constructed
+% according to a common scheme:
+% \begin{itemize}
+% \item The offset (x in "count1" and y in "count2") from the local
+%   origin to the starting position is calculated: If the diagram is
+%   \emph{not} nested, the bottom should be centered around the position
+%   given by "\put". If the diagram  is nested, the bottom should
+%   be at the current vertical position, if the diagram is to be drawn
+%   \emph{upwards}. Conversely, the top should be at the current vertical
+%   position if the diagram is to be drawn \emph{downwards}. If the
+%   diagram should go to the \emph{left}, the right side should be at
+%   the current horizontal position, and conversely.
+% \item A "\hbox" is shifted to the given offset using "\hskip" and
+%   "\raise". Inside the box  the frame of the diagram is drawn first.
+%   This is done using the "\put", "\line" and other
+%   "picture" commands. This relies on the way the
+%   "picture" commands are construtced. It is admittely a little
+%   bad style to use the commands in a non-documented ways, but it takes up a
+%   little less memory, and I would like later to implement most of the
+%   commands using rules, which would be faster.
+% 
+% \item The parameters are parsed. This is done in a specialized macro, to
+%   which the position and orientation (\emph{ie} up and left) of a
+%   possible nested diagram, and the coordinates for the symbol in the
+%   current diagram are given.  The macro will examine the argument, and if it
+%   consists of letters, it is considered a language symbol and is
+%   set in the appropriate place. If itis a macro, however, the nested diagram
+%   will be drawn, returning the language symbol using the global register
+%   "\@@symbol", which afterwards is set inside the diagram.
+% 
+% \item If the diagram is nested, it is finally ensure, that "\@@symbol"
+%   is set globally accordingly to the orientation. Thus it returns
+%   the symbol to the ``calling'' diagram.
+% \end{itemize}
+% 
+% Most of the translation diagrams are coded with a small stup, that
+% packs the arguments (that are separated by commas) followed by an "\end",
+% so that \TeX's pattern matching can separate them.
+% 
+% \begin{macro}{\compiler}
+% \begin{macro}{\@compiler}\mbox{}
+% \changes{1.2$\alpha$}{1996/27/01}{Rewritten to fit with a "picture"-environment and nesting of diagrams}
+%    \begin{macrocode}
+\newcommand{\compiler}[1]{\@compiler#1\end}
+\def\@compiler#1,#2,#3\end{%
+  \if@@Nested %
+    \if@@Up %
+    \@@yShift=40 \if@@Left \@@xShift=-50 \else \@@xShift=-30 \fi
+    \else%
+      \@@yShift=20 \@@xShift =0 %
+    \fi%
+  \else%
+    \@@yShift=40 \@@xShift=-40%
+    \fi
+  \hskip\@@xShift\unitlength\raise \@@yShift\unitlength\hbox{%
+    \put(0,0){\line(1,0){80}}%
+    \put(0,-20){\line(1,0){30}}%
+    \put(50,-20){\line(1,0){30}}%
+    \put(30,-40){\line(1,0){20}}%
+    \put(0,0){\line(0,-1){20}}%
+    \put(80,0){\line(0,-1){20}}%
+    \put(30,-20){\line(0,-1){20}}%
+    \put(50,-20){\line(0,-1){20}}%
+    \put(30,-20){\makebox(20,20){$\rightarrow$}} %
+   {\@@Uptrue \@@Lefttrue \@parseArg(0,-20)(5,-20)#1\end}%
+   \if@@Up \else \@@tempSymbol=\expandafter{\the\@@symbol}\fi
+   {\@@Uptrue \@@Leftfalse \@parseArg(80,-20)(55,-20)#3\end}%
+   {\@@Upfalse \@@Lefttrue \@parseArg(50,-40)(30,-40)#2\end}%
+   \if@@Up \@@tempSymbol=\expandafter{\the\@@symbol}\fi
+    \if@@Nested \global\@@symbol=\expandafter{\the\@@tempSymbol} \fi%
+  }%
+}
+%    \end{macrocode}
+% \end{macro} 
+% \end{macro} 
+%
+% \begin{macro}{\interpreter}
+% \begin{macro}{\@interpreter}\mbox{}
+% \changes{1.0}{1995/18/10}{Translated command names from danish to english}
+% \changes{1.2$\alpha$}{1996/27/01}{Rewritten to fit with a "picture"-environment and nesting of diagrams}
+%    \begin{macrocode}
+\newcommand{\interpreter}[1]{\@interpreter#1\end}
+\def\@interpreter#1,#2\end{%
+  \if@@Nested %
+    \if@@Up %
+    \@@yShift=40 \if@@Left \@@xShift=0 \else \@@xShift=20 \fi
+    \else%
+      \@@yShift=0 \@@xShift =0 %
+    \fi%
+  \else%
+    \@@yShift=40 \@@xShift=10%
+    \fi
+  \hskip\@@xShift\unitlength\raise \@@yShift\unitlength\hbox{%
+    \put(0,0){\line(-1,0){20}}%
+    \put(0,-40){\line(-1,0){20}}%
+    \put(0,0){\line(0,-1){40}}%
+    \put(-20,0){\line(0,-1){40}}%
+   {\@@Uptrue \@@Lefttrue \@parseArg(0,0)(-20,-20)#1\end}%
+   \if@@Up \else \@@tempSymbol=\expandafter{\the\@@symbol}\fi
+   {\@@Upfalse \@@Lefttrue \@parseArg(0,-40)(-20,-40)#2\end}%
+   \if@@Up \@@tempSymbol=\expandafter{\the\@@symbol}\fi
+    \if@@Nested \global\@@symbol=\expandafter{\the\@@tempSymbol} \fi%
+  }%
+}
+%    \end{macrocode}
+% \end{macro} 
+% \end{macro} 
+% 
+% \begin{macro}{\program}
+% \begin{macro}{\@program}\mbox{}
+% \changes{1.2$\alpha$}{1996/27/01}{Command added}
+%    \begin{macrocode}
+\newcommand{\program}[1]{\@program#1\end}
+\def\@program#1,#2\end{%
+  \if@@Nested %
+    \if@@Up %
+    \@@yShift=0 \if@@Left \@@xShift=0 \else \@@xShift=20 \fi
+    \else%
+      \PackageError{semantic}{%
+        A program cannot be at the bottom}
+        {%
+          You have tried to use a \protect\program\space as the
+          bottom\MessageBreak parameter to \protect\compiler,
+          \protect\interpreter\space or \protect\program.\MessageBreak
+         Type <return> to proceed --- Output can be distorted.}%
+    \fi%
+  \else%
+    \@@yShift=0 \@@xShift=10%
+    \fi
+  \hskip\@@xShift\unitlength\raise \@@yShift\unitlength\hbox{%
+    \put(0,0){\line(-1,0){20}}%
+    \put(0,0){\line(0,1){30}}%
+    \put(-20,0){\line(0,1){30}}%
+    \put(-10,30){\oval(20,20)[t]}%
+    \@putSymbol[#1]{-20,20}%
+   {\@@Upfalse \@@Lefttrue \@parseArg(0,0)(-20,0)#2\end}%
+  }%
+}
+%    \end{macrocode}
+% Note that a little code that reports errors if the
+% command is used wrongly, is incorporated.
+% \end{macro} 
+% \end{macro} 
+% 
+% \begin{macro}{\machine}\mbox{}
+% \changes{1.2$\alpha$}{1996/27/01}{Command added}
+%    \begin{macrocode}
+\newcommand{\machine}[1]{%
+  \if@@Nested %
+    \if@@Up %
+      \PackageError{semantic}{%
+        A machine cannot be at the top}
+        {%
+          You have tried to use a \protect\machine\space as a
+          top\MessageBreak parameter to \protect\compiler or
+          \protect\interpreter.\MessageBreak
+         Type <return> to proceed --- Output can be distorted.}%
+       \else \@@yShift=0 \@@xShift=0
+    \fi%
+  \else%
+    \@@yShift=20 \@@xShift=10%
+    \fi
+  \hskip\@@xShift\unitlength\raise \@@yShift\unitlength\hbox{%
+    \put(0,0){\line(-1,0){20}} \put(-20,0){\line(3,-5){10}}
+    \put(0,0){\line(-3,-5){10}}%
+   {\@@Uptrue \@@Lefttrue \@parseArg(0,0)(-20,-15)#1\end}%
+  }%
+}
+%    \end{macrocode}
+% Note that a little code that reports errors if the
+% command is used wrongly, is incorporated.
+% \end{macro} 
+%
+% \begin{macro}{\@parseArg}
+% \begin{macro}{\@getSymbol}
+% \begin{macro}{\@doSymbolMacro}
+% \begin{macro}{\@saveBeforeSymbolMacro}
+%   These macros parse a single argument. As there is some testing of
+%   the following token, it is splitted into four macros, the main one being
+%   "\@parseArg". It is given the offset to a possibly nested diagram and the
+%   position of the symbol within the current diagram. All it does is
+%   testing wether the argument is a command ("\@doSymbolMacro") or some
+%   text string ("@\getSymbol"), and then passing the parameters on to the
+%   appropriate macro.
+%    \begin{macrocode}
+\def\@parseArg(#1)(#2){%
+  \@ifNextMacro{\@doSymbolMacro(#1)(#2)}{\@getSymbol(#2)}}
+%    \end{macrocode}
+%   "\@getSymbol" is used when the argument is ``plain'' text. It simply
+%   passes the parameters to "\@putSymbol", which does the setting up.
+%    \begin{macrocode}
+\def\@getSymbol(#1)#2\end{\@putSymbol[#2]{#1}}
+%    \end{macrocode}
+%   "\@doSymbolMacro" is used when the argument has been identified as a
+%   macro. It tests if there is an optional argument, which is then saved
+%   in "\@@symbol" using "\@saveBeforeSymbolMacro" and "\@@tempSymbol".
+%   Then the macro is expanded.
+%    \begin{macrocode}
+\def\@doSymbolMacro(#1)(#2)#3{%
+  \@ifnextchar[{\@saveBeforeSymbolMacro(#1)(#2)#3}%
+               {\@symbolMacro(#1)(#2)#3}}
+%    \end{macrocode}
+%    \begin{macrocode}
+\def\@saveBeforeSymbolMacro(#1)(#2)#3[#4]#5\end{%
+  \@@tempSymbol={#4}%
+  \@@Nestedtrue\put(#1){#3#5}%
+  \@putSymbol[\the\@@tempSymbol]{#2}}
+%    \end{macrocode}
+%    \begin{macrocode}
+\def\@symbolMacro(#1)(#2)#3\end{%
+  \@@Nestedtrue\put(#1){#3}%
+  \@putSymbol{#2}}
+%    \end{macrocode}
+% \end{macro}
+% \end{macro}
+% \end{macro}
+% \end{macro}
+%
+% \begin{macro}{\@putSymbol}
+%   This is an auxiliary macro that sets as default set the text of register
+%   "\@@symbol" on the given position. If, however, a parameter is given,
+%   "\@@symbol" is set to this parameter before "\@@symbol" is set. The
+%   macro is used by all the diagrams to set the symbols when they have
+%   been determined.
+%    \begin{macrocode}
+\newcommand{\@putSymbol}[2][\the\@@symbol]{%
+  \global\@@symbol=\expandafter{#1}%
+  \put(#2){\makebox(20,20){\texttt{\the\@@symbol}}}}
+%</Tdiagram>
+%    \end{macrocode}
+% \end{macro}
+%
+% \MakeShortVerb{\|} ^^A Usefull as " is used by the grammar
+% \subsection{Reserved words}
+%
+%    \begin{macrocode}
+%<*reservedWords>
+\TestForConflict{\reservestyle,\@reservestyle,\setreserved,\<}
+\TestForConflict{\@parseDefineReserved,\@xparseDefineReserved}
+\TestForConflict{\@defineReserved,\@xdefineReserved}
+%    \end{macrocode}
+%
+% \begin{macro}{\reservestyle}
+%   \changes{2.0$\alpha$}{1996/05/18}{Added commands for setting reserved
+%     words: \CSname{reservestyle} and \CSname{<}}
+%   "\reservestyle" defines the typesetting style for a class of reserved
+%   words by defining a command for defining reserved words
+%   from this class
+%    \begin{macrocode}
+\newcommand{\reservestyle}[3][]{
+  \newcommand{#2}{\@parseDefineReserved{#1}{#3}}
+%    \end{macrocode}
+%   "\reservestyle" takes an optional command to control the spacing, \eg
+%   "\mathinner", a command \CSname{\meta{name}} and a formatting
+%   macro.  The commandname is defined to call an internal parsing function,
+%   "\@parseDefineReserved" which will reserve the concrete words.
+%    \begin{macrocode}
+   \expandafter\expandafter\expandafter\def
+     \expandafter\csname set\expandafter\@gobble\string#2\endcsname##1%
+   {#1{#3{##1}}}}
+%    \end{macrocode}
+%  Defines the command \CSname{set\meta{name}} as a shortcut to get the
+%  specified style.  For an explanation of the expansion of
+%  \CSname{set\meta{name}}, see the definition of "@xdefineReserved" on
+%     p.~\pageref{page:styleExpansion}. 
+% \end{macro} ^^A \reservestyle
+%
+% \begin{macro}{\@parseDefineReserved}^^A 
+% \begin{macro}{\@xparseDefineReserved}^^A
+%   "\@parseDefineReserved" parses the parameters and set up the following
+%   two internal registers, which are used when defining each word.
+%    \begin{macrocode}
+\newtoks\@@spacing
+\newtoks\@@formating
+\def\@parseDefineReserved#1#2{%
+  \@ifnextchar[{\@xparseDefineReserved{#2}}%
+     {\@xparseDefineReserved{#2}[#1]}}
+%    \end{macrocode}
+% If no spacing command is provided to the definition, the default ("#1")
+% for the style is used. 
+%    \begin{macrocode}
+\def\@xparseDefineReserved#1[#2]#3{%
+  \@@formating{#1}%
+  \@@spacing{#2}%
+  \expandafter\@defineReserved#3,\end
+}
+%    \end{macrocode}
+%   The formatting and the spacing information is saved and then the
+%   comma separated list of words to be reserved are processed.  The
+%   sequence ",\end" gives and end marker.
+% \end{macro} ^^A \@parseDefineReserved
+% \end{macro} ^^A \@xparseDefineReserved
+%
+% \begin{macro}{\@defineReserved}^^A
+% \begin{macro}{\@xdefineReserved}
+%   The two commands define a reserved word: "\@defineReserved" testes if
+%   it is the last argument and makes it possible for "\@xdefineReserved" to
+%   test if an alternative text is provided. "\@xdefineReserved" also
+%   defines the reserved word. 
+%    \begin{macrocode}
+\def\@defineReserved#1,{%
+  \@ifnextchar\end
+%    \end{macrocode}
+%   Testes if this is the last word ("\end" is following the comma) to
+%   decide if another iteration should be done after defining the word in
+%   "#1".  
+%    \begin{macrocode}
+  {\@xdefineReserved #1[]\END\@gobble}%
+%    \end{macrocode}
+%   If is was the last then remove the endmarker "\end".
+%    \begin{macrocode}
+  {\@xdefineReserved#1[]\END\@defineReserved}}
+%    \end{macrocode}
+%   "[]" is inserted to ensure "\@xdefineReserved" that all
+%   definitions have a pair of and "\END" makes it possible to remove an
+%   extra set of brackets, if there was already a pair of brackets in "#1".
+%    \begin{macrocode}
+\def\@xdefineReserved#1[#2]#3\END{%
+  \def\reserved@a{#2}%
+  \ifx \reserved@a\empty \toks0{#1}\else \toks0{#2} \fi
+%    \end{macrocode}
+%   If the optional text is empty the word is used as text (saved in token
+%   register 0).
+%    \begin{macrocode}
+    \expandafter\edef\csname\expandafter<#1>\endcsname
+    {\the\@@formating{\the\@@spacing{\the\toks0}}}}
+%    \end{macrocode}
+%   \label{page:styleExpansion}
+%   This defines the reserved word given in "#1" to the text given in
+%   "#2". Saving "#2" in token register 0 is done to avoid having "\edef"
+%   expanding any commands in the text (\see \cite[p.~216]{texbook}).
+%
+%   The reserved words are saved as macros with the names enclosed in angle
+%   brackets. They can thus only be expanded using
+%   "\csname"\lttdots"\endcsname".  The typesetting ("{#1{#3}}") is done 
+%   inside a group so it is possible to use style changing commands like
+%   "\scriptstyle" (though it would admittedly be strange).  By enclosing 
+%   the text "#2" in brackets one argument commands like "\textbf" are also
+%    possible.   
+% 
+%   Be aware that the use of "\def" to
+%   define the command, allows redefinition of a already reserved words an
+%   even other macros.
+% \end{macro} ^^A \@xdefineReserved
+% \end{macro} ^^A \@DefineReserved
+%
+% \begin{macro}{\setreserved}
+% \begin{macro}{\<}
+%   "\setreserved" is a command for internal use (however provided for the
+%   user if necessary to avoid conflict on "\<") to typeset a reserved word.
+%   "\setreserved" is used by "\<",
+%   the command to typeset reserved words, and the argument is thus
+%   delimited by a ">" (the use being "\<"\meta{name}">").
+%    \begin{macrocode}
+\def\setreserved#1>{%
+  \expandafter\let\expandafter\reserved@a\csname<#1>\endcsname
+  \@ifundefined{reserved@a}{\PackageError{Semantic}
+      {``#1'' is not defined as a reserved word}%
+      {Before referring to a name as a reserved word, it % 
+      should be defined\MessageBreak using an appropriate style 
+      definer.  A style definer is defined \MessageBreak 
+      using \protect\reservestyle.\MessageBreak%
+      Type <return> to proceed --- nothing will be set.}}%
+  {\reserved@a}}
+\let\<=\setreserved
+%</reservedWords>
+%    \end{macrocode}
+%   Typesetting of the reserved word is done by expanding the macro defined
+%   for the name.  The macro name is first build in the internal \LaTeX\
+%   register "\reserved@a" so it can be tested if the name is defined. 
+% \end{macro}
+% \end{macro}
+%
+% \subsection{The Short Hands Part}
+% \changes{2.0}{1998/05/24}{Made the short hand options part}
+% At last  come all the commands for symbols facilitating the notation of
+% semantics. They are all fairly simple, taking some arguments and setting
+% them in an  pproriate font intermixed with some filling symbols.
+%
+% \subsubsection{The Symbols \@bblb and \@bbrb}
+% \begin{macro}{\@bblb}
+% \begin{macro}{\@bbrb}
+% \begin{macro}{\@mbblb}
+% \begin{macro}{\@mbbrb}
+% \changes{1.0}{1995/10/20}{I have defined ``fake''-black\-board\-bold for
+% the benefit of  people who do not have \package{bbold}}
+% \changes{1.2$\alpha$}{1996/01/31}{Changed the names}
+% \changes{1.2$\alpha$}{1996/01/31}{Added permanent use of document main font}
+% \makeatletter\changes{2.0}{1998/05/24}{Moved to the new "shorthand" options part and made ligatures for $\@bblb$ and $\@bbrb$.}\makeatother
+% \changes{2.0}{1998/05/24}{Introduced the math mode commands \CSname{@mbblb} and \CSname{@mbbrb}.}
+% \makeatletter
+% If \package{bbold}, is installed it is used to make \@bblb\ og \@bbrb.
+% Otherwise two brackets are drawn together. To make this transparent to the
+% rest of the package, two commands "\@bblb" (\textbf{b}lackboard
+% \textbf{b}old \textbf{l}eft \textbf{b}racket) and "\bbrb"
+% (\textbf{b}lackboard \textbf{b}old \textbf{r}ight \textbf{b}racket) are
+% defined , which in both cases gives \@bblb\ or \@bbrb, respectively.
+%    \begin{macrocode}
+%<*shorthand>
+\IfFileExists{DONOTUSEmathbbol.sty}{%
+  \RequirePackage{mathbbol} 
+  \newcommand{\@bblb}{\textbb{[}}
+  \newcommand{\@bbrb}{\textbb{]}}
+  \newcommand{\@mbblb}{\mathopen{\mbox{\textbb{[}}}}
+  \newcommand{\@mbbrb}{\mathclose{\mbox{\textbb{]}}}}
+} 
+{ \newcommand{\@bblb}{\textnormal{[\kern-.15em[}}
+  \newcommand{\@bbrb}{\textnormal{]\kern-.15em]}}
+  \newcommand{\@mbblb}{\mathopen{[\mkern-2.67mu[}}
+  \newcommand{\@mbbrb}{\mathclose{]\mkern-2.67mu]}}
+}
+%    \end{macrocode}
+% \makeatother
+% \end{macro}
+% \end{macro}
+% \end{macro}
+% \end{macro}
+%
+% \subsubsection{Short Hands for the Often Needed Symbols}
+%
+% This defines the often needed symbols.  Note that by specifying the option
+%  "shorthand" math ligatures are automatically loaded.
+%    \begin{macrocode}
+\mathlig{|-}{\vdash}
+\mathlig{|=}{\models}
+\mathlig{->}{\rightarrow}
+\mathlig{->*}{\mathrel{\rightarrow^*}}
+\mathlig{->+}{\mathrel{\rightarrow^+}}
+\mathlig{-->}{\longrightarrow}
+\mathlig{-->*}{\mathrel{\longrightarrow^*}}
+\mathlig{-->+}{\mathrel{\longrightarrow^+}}
+\mathlig{=>}{\Rightarrow}
+\mathlig{=>*}{\mathrel{\Rightarrow^*}}
+\mathlig{=>+}{\mathrel{\Rightarrow^+}}
+\mathlig{==>}{\Longrightarrow}
+\mathlig{==>*}{\mathrel{\Longrightarrow^*}}
+\mathlig{==>+}{\mathrel{\Longrightarrow^+}}
+\mathlig{<-}{\leftarrow}
+\mathlig{*<-}{\mathrel{{}^*\mkern-1mu\mathord\leftarrow}}
+\mathlig{+<-}{\mathrel{{}^+\mkern-1mu\mathord\leftarrow}}
+\mathlig{<--}{\longleftarrow}
+\mathlig{*<--}{\mathrel{{}^*\mkern-1mu\mathord{\longleftarrow}}}
+\mathlig{+<--}{\mathrel{{}^+\mkern-1mu\mathord{\longleftarrow}}}
+\mathlig{<=}{\Leftarrow}
+\mathlig{*<=}{\mathrel{{}^*\mkern-1mu\mathord\Leftarrow}}
+\mathlig{+<=}{\mathrel{{}^+\mkern-1mu\mathord\Leftarrow}}
+\mathlig{<==}{\Longleftarrow}
+\mathlig{*<==}{\mathrel{{}^*\mkern-1mu\mathord{\Longleftarrow}}}
+\mathlig{+<==}{\mathrel{{}^+\mkern-1mu\mathord{\Longleftarrow}}}
+\mathlig{<->}{\longleftrightarrow}
+\mathlig{<=>}{\Longleftrightarrow}
+\mathlig{|[}{\@mbblb}
+\mathlig{|]}{\@mbbrb}
+%    \end{macrocode}
+% 
+% \subsubsection{Denotational Semantics}
+% I have given a lot of thoughts to the problem of choosing a good syntax.
+% The most essential requirement was that syntax should be consistent and
+% simple/intuitive, close to that used in \emph{Introduction to the Semantics
+%   of Programming Languages}. To a semanticer, the most natural way to get
+%   \eval{\lttdots}{x} would probably appear to be  "\eval["\lttdots"]x"
+% and indeed "\eval**["\lttdots"]x" rather than "\eval[**]{"\lttdots"}{x}".
+% This is however a departure from the standard syntax of \LaTeX. And even
+% more decisively, one cannot make an analogoues syntax for
+% "\evalsymbol" since it is undecidable whether it is followed by a
+% symbol: Does \emph{eg} "\evalsymbol test" mean ``\evalsymbol[t]est'' or
+% ``\evalsymbol test''? This makes it necessary to use brackets in connection
+% with "\evalsymbol" and in order to have a consistent syntax,  I have made
+% the same decission for "\eval".
+%\begin{macro}{\evalsymbol}
+%\begin{macro}{\compsymbol}\mbox{}
+% \changes{1.0}{1995/10/18}{Settled on a syntax and described my considerations} 
+% \changes{1.0}{1995/10/18}{Made som ``cleanup'' based on the decided syntax}
+%    \begin{macrocode}
+\newcommand{\evalsymbol}[1][]{\ensuremath{\mathcal{E}^{#1}}}
+\newcommand{\compsymbol}[1][]{\ensuremath{\mathcal{C}^{#1}}}
+%    \end{macrocode}
+%   These lines define commands that take  an optional argument. If this
+%   argument is \emph{not} present, the default value given in the second
+%   pair of  brackets is used ie.\ nothing.
+% \end{macro}
+% \end{macro}
+%
+%\begin{macro}{\eval}
+%\begin{macro}{\comp}\mbox{}
+% \changes{1.0}{1995/10/18}{Erased several previous commands as they were
+% just  special cases of the other commands (with the decided
+% syntax). Furthermore the names were  translated from danish into english}
+% \changes{1.2$\alpha$}{1996/01/30}{Made a brand new definition to avoid an
+% error when using \CSname{comp} and \CSname{eval} with displaymath}
+%    \begin{macrocode} 
+\newcommand{\eval}[3][]%
+  {\mbox{$\mathcal{E}^{#1}$\@bblb \texttt{#2}\@bbrb}%
+   \ensuremath{\mathtt{#3}}}
+\newcommand{\comp}[3][]%
+  {\mbox{$\mathcal{C}^{#1}$\@bblb \texttt{#2}\@bbrb}%
+   \ensuremath{\mathtt{#3}}}
+%    \end{macrocode}
+%  This definition should allow a linebreak after the last bracket
+% \end{macro}
+% \end{macro}
+%
+% \begin{macro}{\exe} \mbox{}
+% \changes{1.0}{1995/10/18}{Translated the name to english}
+%    \begin{macrocode}
+\newcommand{\@exe}[3]{}
+\newcommand{\exe}[1]{\@ifnextchar[{\@exe{#1}}{\@exe{#1}[]}}
+\def\@exe#1[#2]#3{%
+  \mbox{\@bblb\texttt{#1}\@bbrb$^\mathtt{#2}\mathtt{(#3)}$}}
+%</shorthand>
+%    \end{macrocode}
+%   The command "\exe" is a stub that checks if the second argument begins 
+%   with an optional sharp by looking at the token following the first
+%   argument. If  a bracket  is not provided, an empty second argument is
+%   added before the control is given to "\@exe", which does the setting.
+%   There is no place to do an expedient linebreak, so everything is
+%   encapsulated in a "\mbox".
+% \end{macro}
+%
+% \subsection{End of All Options Files}
+%  
+% All the options files are ended with the following code to match the test
+% whether the file is loaded from the semantics package
+% (\emph{see}~\pageref{page:testForSemanticsLoader}):
+%    \begin{macrocode}
+%<*allOptions>
+\fi
+%</allOptions>
+%    \end{macrocode}
+%
+% \subsection{Preamble of Users Guide and Documentation}
+% \changes{1.0}{1995/10/16}{Made "semantic.sty" into a ".dtx"-file with a stub for generating the users guide and documentation}
+% \changes{1.0}{1995/10/16}{Added control that the requested files is in fact  installed}
+% \changes{1.2$\alpha$}{1996/01/28}{Put the document header at the bottom, and introduced a hack making \LaTeX\ think it is loading \texttt{semantic.sty} when processing \texttt{semantic.dtx}}
+%
+% The document preamble and the code to generate code is placed at the end,
+% so that the documentation may  be printed before \semantic\ is installed. 
+% For the use of \package{docstrip}, the code is marked as conditional
+%   code, so that it is not included in "semantic.sty" when installing the
+% package.
+%    \begin{macrocode}
+%<*documentation>
+\documentclass{ltxdoc} 
+\usepackage[latin1]{inputenc}
+\usepackage[T1]{fontenc}
+ % Checks if the package for multiple columns is installed and if that 
+ % is the case, then load it. Borrowed from the standard package \
+ % ``doc.dtx'' 
+\newif\ifmulticols 
+\IfFileExists{multicol.sty}{\multicolstrue}{}
+
+\newif\ifdanger
+\dangertrue       % Make this line into a comment, if the manual font
+                  % ``manfnt.tfm'' is not installed on your system
+\DeclareFontFamily{U}{manual}{} 
+\DeclareFontShape{U}{manual}{m}{n}{<->  manfnt }{} 
+
+\newcommand{\danger}
+  {{\fontencoding{U}\fontfamily{manual}\selectfont\symbol{127}}}
+
+\OnlyDescription    % Make to a comment to get the documentation
+\DisableCrossrefs   % Remove comment if the index is ready or if you
+                    % do not wish the index (e.g. when only printing
+                    % the users guide)
+% \CodelineIndex      % Make a index of the command usage
+% \RecordChanges      % Make the changes history
+
+\makeatletter
+
+\usepackage{xspace}
+\newcommand{\ie}{\emph{ie}\xspace}
+\newcommand{\eg}{\emph{eg}\xspace}
+\newcommand{\see}{\emph{see}\xspace}
+\newcommand{\semantic}{\texttt{semantic}\xspace}
+\newcommand{\lttdots}{\ensuremath{\mathtt{\ldots}}}
+\newcommand{\ExplicitSpace}{\texttt{\char'040}}
+\newcommand{\CSname}[1]{\texttt{\protect\bslash#1}}
+\newcommand{\package}[1]{\textsf{#1}}
+
+\def\GetInfo#1{%
+  \def\filename{#1}%
+  {\def\ver##1(##2)##3\relax{%
+     \def\tc{##1}%
+     \def\td{##2}%
+     \ifx \td\empty %
+     \else %
+      \edef\td{$\csname ##2\endcsname$}%
+     \fi}%
+   \def\tb##1 v##2 ##3\end{%
+   \gdef\filedate{##1}%
+     \ver ##2()\relax%
+     \xdef\fileversion{\tc\expandafter\noexpand\td}%
+    \gdef\fileinfo{##3}}%
+  \edef\ta{\csname ver@#1\endcsname}%
+  \expandafter\tb\ta\end\relax}}
+
+\newtoks\p@rm@rk 
+\newcommand{\setparagraphmark}[1]{\p@rm@rk={#1}}
+\newcommand{\parmark}[1][\the\p@rm@rk]{%
+  \setbox0=\hbox{\huge #1}%
+  \clubpenalty=10000%
+  \noindent\hangindent=\wd0 \hangafter=-2%
+  \llap{\raise.35em\hbox{\vbox to\z@{\box0 \vss}\hfill}}}
+
+\newenvironment{code}
+  {\begin{verse}\small}
+  {\end{verse}}
+
+\newenvironment{columnItemize}%
+  {\begin{list}%
+    {$\bullet$}%
+    {\settowidth{\labelwidth}{$\bullet$}%
+     \setlength{\leftmargin}{5mm}%
+     \setlength{\labelsep}{\leftmargin}%
+     \addtolength{\labelsep}{-\labelwidth}}}%
+  {\end{list}}
+
+\typeout{}
+\typeout{NOTE: If LaTeX complains}
+\typeout{\@spaces\@spaces Font U/manual/m/n/9 manfnt at %
+  9.0 not loadable: ...}
+\typeout{\@spaces\space\space then comment out the line (around 2700)}
+\typeout{\@spaces\@spaces \protect\dangertrue}
+\typeout{}
+\typeout{There will be some overfull and underfull boxes, %
+           and some moved marginpars.}
+\typeout{Do not bother!!!}
+\typeout{}
+
+\makeatother
+
+\begin{document}
+  \DocInput{semantic.dtx}
+\end{document}
+%</documentation>
+%    \end{macrocode}
+% 
+% The preamble contains the normal choosing of codetables etc., it checks
+% whether 
+% the requested non-standard package can be found, and it defines some
+% commands (described below) for the use of the documentation and types out
+% some ``relaxing'' messages to the users. I do not know
+% any way to check whether a named font is on the system---"\IfFileExist"
+% cannot 
+% be used since it searches the path in---say---"TEXINPUT", while the fonts are
+% searched using the path "TFMINPUT".
+% 
+% The commands defined are described below:
+% \begin{description}
+% \item[\CSname{ifmulticols}] is a conditional ensuring that \TeX\ branches over
+%   parts setting up multiple columns, when this is not provided.
+% \item[\CSname{ifdanger}] is a conditional that tells whether the dangerous bend
+%   sign from \emph{The \TeX-book} is available. The manualfont ("manfnt")
+%   is declared to NFSS and the command "\danger" is defined anyway. It will
+%   however only be used and therefore tried loaded if "\ifdanger" is true.
+% \item[\CSname{semantic}] gives the package symbol (name in a
+%   typewriter-font)
+% \item[\CSname{eg}, \CSname{see}, and \CSname{ie}] Abbreviations written
+%   with emphasis 
+% \item[\CSname{lttdots}] gives ellipsis in a typewriter-font
+% \item[\CSname{CSname}] typesets a command name when this is not possible using 
+%   the standard notation, |"|\lttdots|"|, from \package{ltxdoc} (eg.\ in
+%   headers). Intentionally given a name close to \TeX's "\csname".
+% \item[\CSname{package}] sets the name of \LaTeX-package.
+% \item[\CSname{GetInfo}] defines the commands "\fileversion", "\filedate"
+%   and "\fileinfo", providing information about \semantic\ given in
+%   "\providespackage". It is mainly borrowed from a command with the same
+%   name in \package{ltxdoc} but has been changed to type the additional
+%   greek letter in the package version provided in parenthesis.
+% \item[\CSname{parmark} and \CSname{setparagraphmark}] is used to set a
+% given symbol in front of a paragraph. "\setparagraphmark" defines the
+% symbol to be used by "\parmark" if no argument is given explicit.
+% \item[\texttt{code}] Environment for displaying examples in the Users Guide.
+% \item[\texttt{columnitemize}] Makes an itemization where the bullet is not
+%   indented, since indentation  would make the text too narrow when the
+%   text is set in columns.
+% \end{description}
+%
+% \begin{thebibliography}{1}
+%   \bibitem{texbook}    
+%     \textsc{D.E.~Knuth} \emph{The \TeX-book}, 1994, Addison-Wesley
+%^^A   \bibitem{companinon} 
+%^^A     \textsc{M.~Goosens, F.~Mittelbach, and A.~Samarin} \emph{The \LaTeX{} Companion}, 1994, Addison-Wesley
+%   \bibitem{packagesguide}
+%     \textsc{The \LaTeX3 Project} \emph{\LaTeXe\ for class and packages writers}, 10 June 1995
+%   \bibitem{LaTeXbook}
+%     \textsc{L. Lamport} \emph{\LaTeX\ : a Document preparation system}, 1994, Addison-Wesley
+% \end{thebibliography}
+%
+% \Finale\PrintIndex \sloppy \PrintChanges
+\endinput
+
diff --git a/Master/texmf-dist/source/latex/semantic/semantic.ins b/Master/texmf-dist/source/latex/semantic/semantic.ins
new file mode 100644
index 00000000000..7614a6415b9
--- /dev/null
+++ b/Master/texmf-dist/source/latex/semantic/semantic.ins
@@ -0,0 +1,14 @@
+% Styreprogram til at lave semantik-pakken udfra .dtx filen.
+% Skal blot køres igennem TeX og senere indarbejdes direkte i semantic.dtx.
+\def\batchfile{semantic.ins}
+\input docstrip
+
+\keepsilent
+
+\generateFile{semantic.sty}{f}{\from{semantic.dtx}{general}}
+\generateFile{infernce.sty}{f}{\from{semantic.dtx}{allOptions,inference}}
+\generateFile{ligature.sty}{f}{\from{semantic.dtx}{allOptions,ligature}}
+\generateFile{tdiagram.sty}{f}{\from{semantic.dtx}{allOptions,Tdiagram}}
+\generateFile{reserved.sty}{f}{\from{semantic.dtx}{allOptions,reservedWords}}
+\generateFile{shrthand.sty}{f}{\from{semantic.dtx}{allOptions,shorthand}}
+