% tlaspec92 
%
% version of spec92 DOCUMENT SUBSTYLE -- 25 Nov 91
%    for LaTeX version 2.09
% modified for use with the tla style
%
% Last modified on Thu Feb  1 10:04:00 PST 1996 by lamport
%
% Changed  9 Apr 92 to remove explicit em widths
% Changed  8 Oct 93 to fix minor problem with \@spec
% Changed 31 Aug 94 so Mosaic won't mess up the file.
% Changed 29 Oct 95 to fix problem with comments in LaTeX2e

\typeout{NEW VERSION}
% Defines a `spec' environment for printing my style of specifications.
% The spec environment is like verbatim except for the following
% differences:
%    -- \ has its usual meaning (catcode)
%
%    -- _ and ^ produce sub- and superscripts.  However, because
%       { and } produce symbols, the rules for arguments are different.  
%       A 1-character script can be written like _3 or ^x .  
%       Multi-character arguments are delimited by {...} or (...) or [...] 
%       or <...>.  However, the same delimiter cannot be nested.  You can 
%       write  _[x_{32}] or ^(a[i]).  You cannot write _[x_[32]] or
%       ^(a(i)).
%
%    -- :foo: is translated to $\foo$, and made an integral
%       number of character-widths.  For example, :beta: makes a 
%       1-character wide $\beta$.  More precisely, ":" followed
%       by any nonblank character other than ":" or "=" is assumed
%       to be a command of the form ":xxx:", where "xxx" is a string
%       with no blanks or ":"s.  The command 
%
%          \coloncommand{xxx}{text}
%
%       is like \newcommand{\xxx}{text} except that
%       "xxx" can be any string not containing any of the following
%       five characters: { } \ : %
%       Also, "xxx" cannot consist of the single character * .
%       
%
%    -- Comments are written either like this 
%
%            Optional Text  (* This is a comment *)  Optional Text
%
%       or like this
%
%          Optional Text (*******************************************)
%                        (*   This is a multiline                   *)
%                        (*   comment.                              *)
%                        (*******************************************)
%
%       and formats them as minipages, indented the indicated distance
%       from the left margin and extending to the right margin.
%
%
%       Comments are formatted in a non-\tt font, matching " characters 
%       are handled properly, and > and < work right outside math mode.
%       `foo' is translated to {\tt foo}.
%
%       In comments, $ ^ and _  have their usual TeX meaning.
%       except within `...', where they are literals.
%
%       SURPRISES:
%         * THERE MUST BE A SPACE CHARACTER FOLLOWING the "(*"
%         * BLANK LINES IN A COMMENT ACT LIKE A SINGLE SPACE
%         * DON'T PUT ANY *'s IN A COMMENT.
%         * DON'T PUT TWO *'s IN A ROW EXCEPT AROUND A COMMENT.
%

%    --  A sequence of 4 or more "-"s begins a horizontal line that runs 
%        to the end of the page.  The two basic options are:
% 
%           ------| Text |------   produces      -------- Text --------
%                                               |                      |
% 
%     
%           --------------------   produces     |----------------------|
% 
%        Putting one or more "*"s in the line, any place after the first
%        4 "-"s, causes the ends of the line to "point up" like
%         
%              |                |
%               ----- ...  -----
%
%
%    -- ^L (page break) is equivalent to \newpage
%
%    -- ' is interpreted as a prime rather than a quote
%
%    -- The following transformations are made
%
%         ==    -->  "equals by definition" symbol
%         #     -->  not equal
%         ->    -->  right arrow 
%         <-    -->  left arrow
%         <<    -->  something like \ltlt
%         >>    -->  something like \gtgt
%         [[    -->  two close left brackets
%         ]]    -->  two close right brackets
%         []    -->  Box
%         <>    -->  Diamond
%         =>    -->  double right arrow (implies)
%         /\    -->  logical and (MUST HAVE SPACES AROUND IT, AND 
%                                 MUST NOT END A LINE)
%         \/    -->  logical or  (MUST HAVE SPACES AROUND IT)
%         ||    -->  parallel sign
%         |=    -->  validity symbol
%         |-    -->  provable symbol
%         (+)   -->  \oplus
%         (-)   -->  \ominus
%         <     -->  $<$
%         >     -->  $>$
%         |->   -->  \mapsto
%
%       You can get these combinations to rewrite to something else
%       by redefining the following command names:
%        == : \speceqeq      [[ : \speclblb        |=  : \specvdasheq
%        #  : \specsharp     ]] : \specrbrb        |-  : \specvdashminus
%        -> : \specdashgt    [] : \speclbrb        (+) : \specoplus
%        <- : \specltdash    => : \speceqgt        (-) : \specominus
%        << : \specltlt      /\ : \specvee         |-> : \specmapsto
%        >> : \specgtgt      \/ : \specwedge       ||  : \specvdashvdash  
%
%   --  The transformations of < and > are disabled by the \nomathgreater
%       declaration, and re-enabled by the \mathgreater declaration.  
%
%       The transformation of = is disabled by the \nomathequal
%       declaration, and re-enabled by the \mathequal declaration.  
%
%       Text looks better with the transformations when :leq: or :geq:
%       are mixed in with < and =.  Otherwise, it probably looks just as
%       good without the transformations.
%
%   --  Any series of \'s followed by a space are no-ops
%       (use to align stuff in both the .tex file and the output)
%        WARNING : YOU MUST NOT END A LINE WITH A \ (OR WITH A \ 
%                  FOLLOWED ONLY BY SPACES
%
%   --  \* == no page break between this line and the next
%
%       \+ == Used to start a new input line without a new line of output.
%             Kills everything up to the end of this input line, and then
%             until the next / .  So
%
%               abc\+ any /garbage/ here 
%                 /def
%             
%             is equivalent to abcdef.
%
%   --  "\" has its usual meaning inside a spec environment, so
%       ordinary commands that take no arguments can be used.  
%       However, the space after a command is not gobbled as usual.
%       The sequence :.: is a no-op that can be used to delimit
%       commands--as in \foo:.:abc--or to prevent transformations,
%       as in -:.:> to produce -> instead of \rightarrow.
%
%       Commands that take arguments inside a spec environment must
%       be specially defined with the \speclet command.  If \innerfoo
%       is an ordinary command that takes one argument,
%
%           \speclet{\foo}{\innerfoo} 
%
%       defines \foo inside the spec environment to be the same as 
%       \innerfoo outside, except that \foo has the same argument 
%       conventions as _ and ^.   If \innerfoo has two arguments,
%       you can do the following:
% 
%         \newcommand{\foox}[1]{\begingroup\def\temp{#1}\fooy}
%         \newcommand{\fooz}[1]{\innerfoo{\temp}{#1}\endgroup}
%         \speclet{\foo}{\foox}
%         \speclet{\fooy}{\fooz}
%       
%       This makes \foo(x)[y] mean \innerfoo{x}{y}.
%
%       The command \intmbox{text} puts text in a box whose width
%       is an integral number of character widths.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                     CHARACTER WIDTHS                      %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% \intmbox{foo}  : Puts foo in a box an integral number of 
%                   character-widths wide.
%

%\newlength{\@charwidth}
%\settowidth{\@charwidth}{{\small\tt M}}


\def\intmbox#1{{\tt \sbox{\@tempboxa}{#1}%
  \@tempdima=1\wd\@tempboxa \advance\@tempdima .5\@charwidth\relax
  \@tempcnta = \@tempdima
  \divide \@tempcnta \@charwidth
  \makebox[\@tempcnta\@charwidth]{\usebox{\@tempboxa}}}}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                         CATCODES                          %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% IN SPEC ENVIRONMENT
%
%  space   active         {     other           /     active      
%    #     active         }     other           \       \   
%    $     other          (     active          |     active
%    %     other          )     other           .     other 
%    @     other          [     active          ,     other 
%    &     other          ]     active          :     active
%    _     active         <     active          ;     other 
%    ^     active         >     active          !     other 
%    ~     active         =     active          ?     other 
%    `     active         *     active         0-9    other 
%    '     active         +     other          A-Z    letter
%    "     other          -     active         a-z    letter
%    ^L    active

\catcode`^^L=\active\relax
\let^^L=\newpage

\def\spec@catcodes{\let\do\@makeother 
\dospecials\catcode`\\=0\relax%
\spec@activecatcodes}

\begingroup
\gdef\spec@activecatcodes{%
\catcode`:=\active\relax%     :
\catcode`|=\active\relax%     |
\catcode`~=\active\relax%     ~
\catcode`^=\active\relax%     ^
\catcode`_=\active\relax%     _
\catcode`(=\active\relax%     (
\catcode`*=\active\relax%     *
\catcode`'=\active\relax%     '
\catcode`##=\active\relax%    #
\catcode`<=\active\relax%     <
\catcode`-=\active\relax%     -
\catcode`>=\active\relax%     >
\catcode`]=\active\relax%     ]
\catcode`/=\active\relax%     /
\catcode`[=\active\relax%     [
\catcode`=\active\relax%      =
\catcode``\active\relax%      `
\@vobeyspaces%               space 
}      
\endgroup

\def\@prespecsetup{%
\def\/{\specvee}%
\def\@xobeysp{\leavevmode\penalty10000\ \strut}%       
}

% Define \@postspecsetup
\begingroup
\spec@activecatcodes%
\gdef\@postspecsetup{%
\let:\@colon%
\let(\@specleftparen%
\if@superscripts\let^\@makesuper\else\let^\@caret\fi%
\if@subscripts\let_\@makesub\else\let_\@under\fi%
\let\\\relax%
\let~\@spectilde%
\let\*\nopagebreak%   \* == \nopagebreak
\def\.{\relax}%       \. == \relax
\let\+\@nonewline%    \+ == \@nonewline
\let*\@specstar%
\let'\@specprime%
\let#\specsharp%
\let<\@speclt%
\let-\@specdash%
\let>\@specgt%
\let[\@speclbrack%
\let]\@specrbrack%
\let/\@specslash%
\let|\@specvdash
\let=\@speceq}
\endgroup

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%               \spec... DEFAULT DEFINITIONS                %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\def\specvee{\makebox[2\@charwidth]{$\lor$}}           % \/
\def\specwedge{\makebox[2\@charwidth]{$\land$}}        % /\
\def\speceqgt{\makebox[2\@charwidth]{$\Rightarrow$}}   % =>
\def\specltlt{\makebox[2\@charwidth]{{\tt%             % <<
    \char'74\hspace{-.5\@charwidth}\char'74}}}
\def\specgtgt{\makebox[2\@charwidth]{{\tt%             % >>
    \char'76\hspace{-.5\@charwidth}\char'76}}}
\def\speceqeq{\makebox[2\@charwidth]{$%                % ==
   \stackrel{\scriptscriptstyle\Delta}{=}$}}
\def\speclblb{\makebox[2\@charwidth]{{\tt%             % [[
   \char'133\hspace{-.35\@charwidth}\char'133}}}
\def\specrbrb{\makebox[2\@charwidth]{{\tt%             % ]]
   \char'135\hspace{-.35\@charwidth}\char'135}}}
\def\specsharp{\if@mathequal\intmbox{$\neq$}\else%
     \mbox{\tt =\hspace{-\@charwidth}/}\fi}            % #
\def\specequal{\if@mathequal%
    \intmbox{$=$}\else=\fi}                            % = 
\def\specdashgt{\makebox[2\@charwidth]{$\rightarrow$}} % ->
\def\specltdash{\makebox[2\@charwidth]{$\leftarrow$}}  % <-
\def\speccoloncolon{\makebox[\@charwidth]{%            % ::
  \@realcolon\hspace{-.5\@charwidth}\@realcolon}}
\def\speccolonequal{:=}                                % :=
\def\specltgt{\makebox[2\@charwidth]{\boldmath%        % <>
   $\Diamond$}}
\def\speclbrb{\makebox[2\@charwidth]{\boldmath$\Box$}} % []
\def\spectilde{\makebox[\@charwidth]{\scriptsize%      % ~
   $\neg$}}
\def\spectildegt{\makebox[2\@charwidth]{\boldmath%     % ~>
   $\leadsto$}}   
\def\specvdashvdash{\makebox[2\@charwidth]{\boldmath%  % ||
  $\|$}}
\def\specvdasheq{\makebox[2\@charwidth]{\boldmath%     % |=
  $\models$}}
\def\specvdashminus{\makebox[2\@charwidth]{\boldmath%  % |-
  $\vdash$}}
\def\specoplus{\makebox[\@charwidth]{\boldmath%        % (+)
   $\oplus$}}
\def\specominus{\makebox[\@charwidth]{\boldmath%       % (-)
   $\ominus$}}
\def\specmapsto{\makebox[2\@charwidth]{\boldmath%      % |->
  $\mapsto$}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%          HORIZONTAL LINES FOR MODULE SPECS         %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\newlength{\boxrulewd}\setlength{\boxrulewd}{.4pt}
%\newlength{\boxindent}\setlength{\boxindent}{22\@charwidth}
%\newlength{\boxlineht}\setlength{\boxlineht}{.5\baselineskip}
%\newcommand{\boxsep}{\@charwidth}
%\newlength{\boxruleht}
%\newlength{\boxruledp}
%\newcommand{\@computerule}{%
%  \setlength{\boxruleht}{.55ex}%  8 Oct 93 Changed from .5ex because 
%  \setlength{\boxruledp}{-\boxruleht}%     of change to \@spec
%  \addtolength{\boxruledp}{\boxrulewd}}
%\newcommand{\boxrule}{\leaders\hrule height \boxruleht depth \boxruledp
%                      \hfill\mbox{}}

%\newcommand{\@nmlineraise}{\if@botline -\boxrulewd
%    \else-\boxlineht\fi}
%\newcommand{\nameline}[1]{\hspace*{-\boxsep}%
%    \raisebox{\@nmlineraise}[0pt][0pt]{\rule[.5ex]{\boxrulewd
%               }{\boxlineht}}%
%    \boxrule
%    #1\boxrule
%    \raisebox{\@nmlineraise}[0pt][0pt]{\rule[.5ex]{\boxrulewd
%               }{\boxlineht}}\hspace{-\boxsep}\vspace{.5\baselineskip}}

\newcommand{\midline}{\hspace{-\boxsep}%
    \raisebox{-.5\boxlineht}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}%
     \boxrule
    \raisebox{-.5\boxlineht}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}\hspace{-\boxsep}}

\newcommand{\botline}{\hspace{-\boxsep}%
    \raisebox{-\boxrulewd}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}%
     \boxrule
    \raisebox{-\boxrulewd}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}\hspace{-\boxsep}}

\newif\if@nameline
\newif\if@botline

\newcommand{\@modname}{}

\newcommand{\@makeline}{\if@nameline \nameline{\@modname}%
  \else \if@botline \botline \else \midline \fi\fi}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                  COMMENT BRACES                     %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\def\@lcbrace{\makebox[0pt][r]{$\{$}}
%\def\@rcbrace{\@italcorrection\mbox{$\}$}}
\def\@lcbrace{}   % comment braces removed 29 Aug 91
\def\@rcbrace{}   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%               NEW MATH MODE COMMANDS                %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\A}{\makebox[\@charwidth]{\boldmath $\forall$}}
\newcommand{\E}{\makebox[\@charwidth]{\boldmath $\exists$}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%              ARROWS AND DASHES                      %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\def\mbonem#1{\makebox[2\@charwidth]{#1}}
\begingroup
\spec@activecatcodes
\gdef\@speclt{\@nsifnextchar-{\@speclftarrow}{\@xspeclt}}%
\gdef\@xspeclt{\@nsifnextchar<{\@specltlt}{\@yspeclt}}%
\gdef\@yspeclt{\@nsifnextchar>{\@specdmd}{\if@comment\@lt%
\else\@specless\fi}}
\gdef\@specgt{\@nsifnextchar>{\@specgtgt}{\@xspecgt}}%
\gdef\@xspecgt{\if@comment\@gt\else\@specgreater\fi}%
\gdef\@specdash{\@nsifnextchar>{\@specrtarrow}{\@xspecdash}}%
\gdef\@xspecdash{\@nsifnextchar-{\@xxspecdash}{\if@comment\@commentdash%
\else\@dash\fi}}%
\gdef\@xxspecdash-{\@nsifnextchar-{\@xxxspecdash}{\@commentddash}}%
\gdef\@xxxspecdash-{\@botlinefalse\@namelinefalse%
\@nsifnextchar-{\@gobbledash}{\@commentdddash}}%
\gdef\@trygobbledash{\@nsifnextchar-{\@gobbledash}{\@endofdashes}}%
\gdef\@gobbledash-{\@nsifnextchar-{\@gobbledash}{\@endofdashes}}%
\gdef\@endofdashes{\@nsifnextchar*{\@innerbotline}{\@trymodname}}%
\gdef\@innerbotline*{\@botlinetrue\@trygobbledash}%
\gdef\@trymodname{\@nsifnextchar|{\@getmodname}{\@makeline}}%
\gdef\@innermidline-{\midline}
\gdef\@specrtarrow>{\specdashgt}%
\gdef\@speclftarrow-{\specltdash}%
\gdef\@specgtgt>{\specgtgt}%
\gdef\@specltlt<{\specltlt}%
\gdef\@specdmd>{\specltgt}%
\gdef\@specbox]{\speclbrb}%
\gdef\@speclbrack{\@nsifnextchar]{\@specbox}{\@xspeclbrack}}%
\gdef\@specrbrack{\@nsifnextchar]{\@specrbrb}{\@realrb}}%
\gdef\@xspeclbrack{\@nsifnextchar[{\@speclblb}{\@reallb}}%
\gdef\@speclblb[{\speclblb}%
\gdef\@specrbrb]{\specrbrb}%
\gdef\@specslash{\@nsifnextchar\ {\@xand}{\@slash}}%
\gdef\@xand\ {{\specwedge} }%
\endgroup

% special hack needed to define something with argument
\begingroup
\catcode`|=\active\relax%     -
\catcode`-=\active\relax%     -
\gdef\@getmodname|#1|{\def\@modname{#1}\@namelinetrue\@trygobbledash}
\endgroup

\def\@slash{/}
\def\@dash{-}
\def\@commentdash{-\hspace{-.5\@charwidth}-}%{$-$}
\def\@commentddash{--}
\def\@commentdddash{---}
\def\@reallb{[}
\def\@realrb{]}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                   <  AND  >                         %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% \mathgreater causes the transformations 
%                <  -> $<$ 
%                >  -> $>$
\newif\if@mathgreater \@mathgreatertrue
\newcommand{\mathgreater}{\@mathgreatertrue}
\newcommand{\nomathgreater}{\@mathgreaterfalse}
\newcommand{\@specgreater}{\if@mathgreater\intmbox{$>$}\else\char62\relax\fi}
\newcommand{\@specless}{\if@mathgreater\intmbox{$<$}\else\char60\relax\fi}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                   =  AND  #                         %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% \mathequal causes the transformations 
%                =  -> $=$ 
%                #  -> $\neq$
\newif\if@mathequal \@mathequaltrue
\newcommand{\mathequal}{\@mathequaltrue}
\newcommand{\nomathequal}{\@mathequalfalse}


% Defines the formatting of one-line comments
\def\@beginlinecomment{\begingroup\@commenttrue\catcode`"=\active
\catcode`'=12\relax\@fixcomments\@fixspace
 % \catcode`{=1\relax\catcode`}=2\relax
\@fixdollar \catcode`{=\active\relax\catcode`}=\active\relax\@fixbraces
  %\catcode`-=12\relax
\footnotesize\sl\nonfrenchspacing     % comments changed to \footnotesize
\@lcbrace\ignorespaces}               % 29 Aug 91

% Defines formatting of multi-line comments
\newlength{\@commentindent}
\def\@begincomment{\hspace*{\@commentindent}\strut\advance\@commentindent 
-\textwidth\begingroup\minipage[t]{-\@commentindent}
\@commenttrue\catcode`"=\active
\catcode`'=12\relax\@fixcomments\@fixspace
 % \catcode`{=1\relax\catcode`}=2\relax
\@fixdollar
\catcode`{=\active\relax\catcode`}=\active\relax\@fixbraces
 % \catcode`-=12\relax
\nonfrenchspacing
\let\@endcomment\@endcommentline\footnotesize
\sl\makebox\@lcbrace\ignorespaces}


\begingroup
\catcode`$=12\relax
\catcode`^=12\relax
\catcode`_=12\relax
\gdef\@fixdollar{\catcode`$=3\relax
\catcode`^=7\relax\catcode`_=8\relax}
\endgroup

% The following redefines : so it works right inside a comment.
% Needed because space has catcode 10 in the comment.
\begingroup
\catcode` =\active\relax%
\gdef\@fixspace{\catcode` =10\relax\@refixcolon}%
\endgroup

\begingroup
\catcode`:=\active
\gdef\@refixcolon{\def\@colon{\@ifspace{\relax
\@realcolon}{\@nspcolon}}\let:\@colon
\def\@nspcolon{\@ifnextchar:{\@dblcolon}{\@xcmdcolon}}}
\endgroup

% \@ifspace{A}{B} executes A if the next token is a space token,
% else it executes B and replaces next token.
%
% \@nsifnextchar like \@ifnextchar, except it doesn't skip over
% space tokens.

\def\@ifspace#1#2{\def\@tempa{#1}\def\@tempb{#2}\futurelet\@tempc\@ifspacex}
\def\@ifspacex{\ifx\@sptoken\@tempc\let\@tempd\@tempa\else
     \let\@tempd\@tempb\fi\@tempd}

\def\@nsifnextchar#1#2#3{\let\@tempe #1\def\@tempa{#2}\def\@tempb{#3}\futurelet
    \@tempc\@ifnsnch}
\def\@ifnsnch{\ifx \@tempc \@tempe\let\@tempd\@tempa\else\let\@tempd\@tempb\fi
      \@tempd}


% Defines \@fixbraces to make braces show up; used in comments
%
\begingroup
\catcode`{=\active
\catcode`}=\active
\catcode`[=1\relax \catcode`]=2\relax
\gdef\@fixbraces[\let{=\@lcbrack \let}=\@rcbrack]
\endgroup
\def\@lcbrack{\mbox{$\{$}}
\def\@rcbrack{\mbox{$\}$}}

% Make ", <, and > work right in comments
%
\begingroup
\catcode`"=\active\relax
\catcode`<=\active\relax \catcode`>=\active
\catcode``=\active\relax
\gdef\@fixcomments{\let"=\@altquotes%
  \def`{\begingroup
    \catcode'44=12\relax  % $
    \catcode'137=12\relax % _
    \catcode'136=12\relax % ^
    \catcode'55=12\relax  % -
    \let<=\@specless      % <
    \let>=\@specgreater   % >
%    \catcode'74=12\relax  % <
%    \catcode'76=12\relax  % >
%    \catcode'75=12\relax  % =
    \@nsifnextchar{`}{\@altssquote}{\@altsquote}}\@lqtrue}%
\endgroup
\begingroup
\catcode`'=12\relax
\gdef\@altsquote#1'{{\tt\frenchspacing #1}\endgroup}
\catcode``=\active
\gdef\@altssquote`#1''{{\tt\frenchspacing \char"60\relax
              #1\char "27\relax}\endgroup}
\endgroup
\def\@altquotes{\if@lq ``\@lqfalse\else''\@lqtrue\fi}
\newif\if@lq 
\newif\if@comment \@commentfalse
\def\@lt{\mbox{$<$}}
\def\@gt{\mbox{$>$}}

\def\@specundef{ undefined}
% The following \gdef's define commands that must gobble characters
% such as * or : that follow them.
\begingroup
\@vobeyspaces
\catcode`>=\active
\catcode`:=\active%
\catcode`(=\active%
\catcode`-=\active%
\gdef\@colon{\@ifnextchar {\@realcolon}{\@nspcolon}}%
\global\let:=\@colon%
\gdef\@nspcolon{\@ifnextchar:{\@dblcolon}{\@xcmdcolon}}%
%\gdef\@cmdcolon#1:{\expandafter\let\expandafter\@tempa\csname#1\endcsname%
%\intmbox{$\@tempa$}}%
\gdef\@cmdcolon#1:{\begingroup\@cmdcolonlet%        %% changed 25 Nov 91
\expandafter\global\expandafter\let\expandafter\@tempaxs\csname#1\endcsname%
\endgroup\ifx\@tempaxs\relax\@warning%
{\@realcolon#1\@realcolon\@specundef}\fi\intmbox{$\@tempaxs$}}%
\gdef\@dblcolon:{\speccoloncolon}%
\catcode`*=\active%
\gdef\@specstar{\@nsifnextchar*{}{\@sspecstar}}%
\gdef\@sspecstar{\@nsifnextchar){\@endcomment}{\@realstar}}%
\gdef\@endcomment){\unskip\@rcbrace\endgroup}%
\gdef\@specleftparen{\@nsifnextchar*{\@speclpstar}{\@specleftparenx}}%
\gdef\@specleftparenx{\@nsifnextchar+{\@speclpplus}{\@specleftpareny}}%
\gdef\@specleftpareny{\@nsifnextchar-{\@speclpminus}{\@realleftparen}}%
\gdef\@speclpplus+{\@nsifnextchar){\@specoplus}{\@reallpplus}}%
\gdef\@speclpminus-{\@nsifnextchar){\@specominus}{\@reallpminus}}%
\gdef\@specoplus){\specoplus}%
\gdef\@specominus){\specominus}%
\gdef\@speclpstar*{\@nsifnextchar*{\@rowofstars}{\@xbeglinecom}}%
\gdef\@rowofstars#1){\@specxcr}%
\gdef\@endcommentline#1(*{\@nsifnextchar*{\@xendcomment}{\ignorespaces}}
\gdef\@xendcomment#1){\unskip\@rcbrace\endminipage
\vspace{\botcommentskip\baselineskip}\endgroup}
\catcode`=\active%
\gdef\@speceq{\@nsifnextchar={\@dbleql}{\@xspeceq}}%
\gdef\@xspeceq{\@nsifnextchar>{\@eqimpl}{\specequal}}%
\gdef\@dbleql={\speceqeq}
\gdef\@eqimpl>{\speceqgt}
\catcode`\ \active\gdef\@xbeglinecom {\@beginlinecomment}%
\endgroup


\def\@specprime{\makebox[\@charwidth][l]{$\,^{\prime}$}}
\let\@italcorrection\/ 
\def\@realcolon{\if@comment{\@italcorrection\rm :}\@\else:\fi}
\def\@realleftparen{(}
\def\@realstar{*}
\def\@reallpplus{(+}
\def\@reallpminus{(-}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%       DEFINITION OF spec ENVIRONMENT                      %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\def\spec{\@spec\frenchspacing\@chend}

% 8 Oct 93 : Moved \@computerule inside \small, as suggested
%            by Denis B. Roegel
% 29 Nov 95 : replaced \@noligs by \@oldnoligs to compensate for change
%             to \@noligs in LaTeX2e
%
\def\@spec{\trivlist \begingroup\small \@computerule
\baselineskip .75\baselineskip \lineskip\z@ 
\item[]\if@minipage\else\vskip\parskip\fi
\leftskip\@totalleftmargin\rightskip\z@
\parindent\z@\parfillskip\@flushglue\parskip\z@
\@tempswafalse \def\par{\if@tempswa\hbox{}\fi\@tempswatrue\@@par}
\@prespecsetup
\obeylines \tt \catcode``=13 \@oldnoligs
\@postspecsetup
\spec@catcodes}

\begingroup
\catcode``=13
\gdef\@oldnoligs{\let`=\@lquote}
\endgroup

\def\endspec{\endgroup\endtrivlist}

% Defines \end{spec}
%
\begingroup \catcode `[= 1
\catcode`]=2 \catcode `\{=12 \catcode `\}=12
\gdef\@chend[\def\end{spec}[\@xend[spec]]]
\endgroup
\def\@xend{}
\let\@xend=\end




% Defines 
%  \@specxcr == gobble up to <CR>
%                \par 
%                add -\topcommentskip\baselineskip vertical space, 
%                \@commentindent == width of spaces up til next (*
%                \@begincomment
%                 
%  \@xcmdcolon == IF next char = <CR> THEN \@realcolon
%                                     ELSE \@ycmdcolon
%                 FI
%  \@ycmdcolon == IF next char = "=" THEN \@colonequal
%                                    ELSE \@cmdcolon
%                 FI

\begingroup
\catcode`=\active\relax%
\catcode`\^^M\active\relax%
\catcode`*\active\relax\catcode`(\active\relax%
\gdef\@specxcr#1
#2(*{\par\vskip-\topcommentskip\baselineskip\settowidth%
{\@commentindent}{#2}\@begincomment}%
\gdef\@xcmdcolon{\@ifnextchar
{\@realcolon}{\@ycmdcolon}}%
\gdef\@ycmdcolon{\@ifnextchar={\@colonequal}{\@cmdcolon}}%
\gdef\@colonequal#1={\speccolonequal}
\endgroup

\def\topcommentskip{1.3}   %% Changed from 1.0 on 1 Feb 96 to make
                           %%    /\ (**********************)  
                           %%       (* comment            *)
                           %%       (**********************)  
                           %% line up "comment" with "/\"
\def\botcommentskip{.4}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                \speclet                             %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%

{\catcode`[=\active
\catcode`]=\active
\catcode`(=\active
\catcode`<=\active
\catcode`>=\active
\catcode`;=1          % ; = left brace, ' = right brace
\catcode`'=2
\catcode`{=12
\catcode`}=12
\gdef\@getspecarg#1;\@ifnextchar[%
    ;\@specbktarg;#1''%
    ;\@ifnextchar(%
      ;\@specpararg;#1''%
      ;\@ifnextchar<%
         ;\@specanglearg;#1''%
         ;\@ifnextchar{%  }
            ;\@specbracearg;#1''%
            ;\@specshortarg;#1''''''
\gdef\@specbktarg#1[#2];#1;#2''
\gdef\@specpararg#1(#2);#1;#2''
\gdef\@specanglearg#1<#2>;#1;#2''
\gdef\@specbracearg#1{#2};#1;#2''
\gdef\@specshortarg#1#2;#1;#2''
'
\def\speclet#1#2{\newcommand{#1}{\@getspecarg{#2}}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                SUB- AND SUPERSCRIPTS                %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% \superscripts : makes ^X turn into super-X.
% \subscripts   : makes _X turn into sub-X.
% \nosuperscripts, \nosubscripts are inverse declarations
%  Default is with sub- and super-scripts turned on.

\newif\if@subscripts \@subscriptstrue
\newif\if@superscripts \@superscriptstrue
\newcommand{\superscripts}{\@superscriptstrue}
\newcommand{\subscripts}{\@subscriptstrue}
\newcommand{\nosuperscripts}{\@superscriptsfalse}
\newcommand{\nosubscripts}{\@subscriptsfalse}
\newcommand{\@under}{\char '137\relax}
\newcommand{\@caret}{\char '136\relax}

\def\@specsub#1{\@mathcmd{{}_{\raisebox{-.4ex}{\tt #1}}}}
\def\@specsuper#1{\@mathcmd{{}^{\tt #1}}}
\speclet{\@makesub}{\@specsub}
\speclet{\@makesuper}{\@specsuper}

\def\@mathcmd#1{\relax\ifmmode #1\else $#1$\fi}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                   :command:                         %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% \spec@cmdcolonlet : \let's characters made active 
%     in spec environment to expand to themselves
%     For example, \let's ( to \@selflparent
%
% \@actives@to@other : \recatcodes characters normally
%     active in spec environment to other
%
% \@rest@to@other : \recatcodes characters normally
%     not active in spec environment but normally not "other"
%     to "other".
%
% \coloncommand{name}{text} : defines :name: to expand to
%          $text$ inside a spec environment, where :name:
%          can contain any character except { } \ : or * .
%          Note: name may not begin with "=" (since := is a recognized
%          group.
%
\begingroup
\spec@activecatcodes
\gdef\@cmdcolonlet{%
\let|\@selfbar%        |
\let~\@selftilde%      ~
\let^\@selfcaret%      ^
\let_\@selfunderscore% _
\let(\@selflparen%     (
\let*\@selfstar%       *
\let'\@selfrquote%     '
\let#\@selfsharp%     #
\let<\@selflt%         <
\let-\@selfdash%       -
\let>\@selfgt%         >
\let]\@selfrbracket%   ]
\let/\@selfslash%      /
\let[\@selflbracket%   [
\let=\@selfequal%      =
\let`\@selflquote%     `
}
\endgroup

\begingroup
\gdef\@rest@to@other{%
\catcode`$=12\relax%     $
\catcode`&=12\relax%     &
\catcode`"=12\relax%     "
}
\endgroup

\def\coloncommand{%
\begingroup
\@actives@to@other
\@rest@to@other 
\@coloncommand}

\def\@coloncommand#1{\gdef\@coloncmdfoo{#1}\endgroup\@coloncommandx}

\def\@coloncommandx#1{\expandafter\def\csname\@coloncmdfoo\endcsname{#1}}

\gdef\@actives@to@other{% 
\catcode`|=12\relax%     |
\catcode`~=12\relax%     ~
\catcode`^=12\relax%     ^
\catcode`_=12\relax%     _
\catcode`(=12\relax%     (
\catcode`*=12\relax%     *
\catcode`'=12\relax%     '
\catcode`##=12\relax%    #
\catcode`<=12\relax%     <
\catcode`-=12\relax%     -
\catcode`>=12\relax%     >
\catcode`]=12\relax%     ]
\catcode`/=12\relax%     /
\catcode`[=12\relax%     [
\catcode`=12\relax%      =
\catcode``12\relax%      `
}
%
\begingroup
\@actives@to@other
\gdef\@selfbar{|}%         |
\gdef\@selftilde{~}%       ~
\gdef\@selfcaret{^}%       ^
\gdef\@selfunderscore{_}%  _
\gdef\@selflparen{(}%      (
\gdef\@selfstar{*}%        *
\gdef\@selfrquote{'}%      '
\gdef\@selfsharp{#}%       #
\gdef\@selflt{<}%          <
\gdef\@selfdash{-}%        -
\gdef\@selfgt{>}%          >
\gdef\@selfrbracket{]}%    ]
\gdef\@selfslash{/}%       /
\gdef\@selflbracket{[}%    [
\gdef\@selfequal{=}%       =
\gdef\@selflquote{`}%      `
\endgroup

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                       TILDE                         %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
\let\@tilde~
\begingroup
\catcode`~=\active
\catcode`>=\active
\gdef\@spectilde{\@nsifnextchar>{\@specldsto}{\spectilde}}
\gdef\@specldsto>{\spectildegt}
\endgroup

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                       VDASH                         %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
\begingroup
\spec@activecatcodes
\gdef\@specvdash{\@nsifnextchar|{\@specdblvdash}{\@xspecvdash}}%
\gdef\@specdblvdash|{\specvdashvdash}%
\gdef\@xspecvdash{\@nsifnextchar-{\@specvdashminus}{\@yspecvdash}}%
\gdef\@specvdashminus-{\specvdashminus}%
\gdef\@yspecvdash{\@nsifnextchar={\@specvdasheq}{\@realvdash}}%
\gdef\@specvdasheq={\specvdasheq}%
\endgroup

\def\@realvdash{|}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                       |->                           %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
\begingroup%
\spec@activecatcodes% 
\gdef\@specvdashminus-{\@nsifnextchar>{\@specmapsto}{\specvdashminus}}% 
\gdef\@specmapsto>{\specmapsto}%
\endgroup


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                       \+                            %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% \+ == kill everything up to first > on next line.
%       
\begingroup
\catcode`/\active\relax%
\catcode`\^^M\active\relax%
\gdef\@nonewline#1
#2/{}%
\endgroup

%%%%% END OF FILE
