\input fullpage.sty
\input bnf.sty
\input eqnarray.sty
\input oldlfont.sty
\input amssymb.sty

%%  Modifications to bnf.sty

\newcommand{\pto}{\mathop{\rightharpoonup}}     % partial function space


\def\bnf{%
   \mathcode`"=\mathactive
%   \mathcode`[=\mathactive \mathcode`\]=\mathactive
   \mathcode`(=\mathactive \mathcode`\)=\mathactive
   \mathcode`|=\mathactive \mathcode`-=\mathactive
   \mathcode`<=\mathactive \mathcode`\>=\mathactive
   \mathcode`@=\mathactive \mathcode`==\mathactive
   \mathcode96 \mathactive
}

\def\endbnf{\global\@ignoretrue}

\begingroup
  \catcode`\~=\active
  \lccode`\~=`\^^M
  \lowercase{\endgroup
    \gdef\Terminal{\relax\PreTerminal
      \ifmmode \hbox \else \leavevmode\null \fi
      \bgroup
      \TerminalFont
      \catcode`~\active
      \def~{\egroup\@latexerr{Terminal string ended by
                              end of line.}\@ehc}%
    \let\do\@makeother \dospecials \@vobeyspaces \frenchspacing
    \@sTerminal}}

\begingroup
    \catcode`@\active

    \gdef@{% either an escape char or a star group
        \ifnonterminal
            \expandafter\NotInNonTerminal
        \fi
    }%

\endgroup

%%  End of modifications to bnf.sty

%\def\kopt{{\le 1}}
\def\kopt{?}

\def\hatop#1{\hbox{\tt<<\,#1\,>>}}
%\def\hatop#1{\hbox{\tt \#\%#1}}

\def\nil-builtin{\hbox{\tt ()}}

\def\escp{\hbox{$\hatop{escape-procedure}$}}

\def\labelenumi{(\theenumi)}

\def\FV{\mathop{\hbox{FreeV}}\nolimits}

\def\BiV{\mathop{\hbox{BindV}}\nolimits}

\def\BoV{\mathop{\hbox{BoundV}}\nolimits}

\def\FreeOcc{\mathop{\hbox{FreeO}}\nolimits}

\def\BoundOcc{\mathop{\hbox{BoundO}}\nolimits}

\def\SystemEval{\mathop{\hbox{System-Eval}}\nolimits}

\def\Eval{\mathop{\hbox{Eval}}\nolimits}

\def\initglobal{\mathop{C_{\hbox{\scriptsize init}}}\nolimits}

%%\def\Code#1{\hbox{\frenchspacing\tt#1}}

\newtoks\old@everyhbox

\def\Code{%
    \old@everyhbox=\expandafter{\the\everyhbox}%
    \everyhbox=\expandafter{%
        \the\everyhbox
        \tt\frenchspacing
        \global\everyhbox=\expandafter{\the\old@everyhbox}%
    }%
    \hbox
}

\let\aless\prec

\let\rulesto\longrightarrow

\def\trans{\mathbin{\mathop{\rulesto}\limits_{\rm trans}}}

\def\eval1{\mathbin{\mathop{\rulesto}\limits_{\rm eval}}}

\def\rewrite1{\mathbin{\mathop{\rulesto}\limits_{\rm rew}}}

\def\grbg1{\mathbin{\mathop{\rulesto}\limits_{\rm grbg}}}

\def\valof{\mathop{\hbox{Value}}\nolimits}

\def\numval{\mathop{\hbox{Numval}}\nolimits}

\def\simpval{\mathop{\hbox{Simpval}}\nolimits}

\def\exp{\hbox{$\bnf <exp>$}}

\def\var{\hbox{$\bnf <var>$}}

\def\body{\hbox{$\bnf <body>$}}

\def\constant{\hbox{$\bnf <constant>$}}

\def\value{\hbox{$\bnf <value>$}}

\def\lrfval{\hbox{$\bnf <non-letrec-val>$}}

\def\nlevalcl{\hbox{$\bnf <nonletrec-evalctxt>$}}

\def\pairval{\hbox{$\bnf <pair-val>$}}

\def\fval{\hbox{$\bnf <false-value>$}}

\def\err-mes{\hbox{$\hatop{error-message}$}}

\let\union\cup
\let\intersect\cap

\newcommand{\rstrct}[2]{#1 \restriction #2}

\newcommand{\cov}[2]{#1+#2}  %or some other connective

\def\dom{\mathop{\hbox{domain}}\nolimits}

\def\ran{\mathop{\hbox{range}}\nolimits}

\def\suchthat{|}

\def\r4s{\hbox{Revised$^4$ Scheme}}

%\def\true{V_{\rm true}}

%\def\false{V_{\rm false}}

\def\T{\hbox{\tt\#t}}
\def\F{\hbox{\tt\#f}}

\newcommand{\ext}[2]{\mbox{$#1 \oplus #2$}}
\newcommand{\selectlet}[1]{$ \cal{S}_{\rm let}[\hbox{#1}] $}
\newcommand{\selectletrec}[1]{$ \cal{S}_{\rm letrec}[\hbox{#1}] $}

\newcount\kludgecount

\def\labelitemii{$\bullet\bullet$}

\def\traggedright{\@rightskip\@flushglue \rightskip\@rightskip
  \leftskip\z@
  \parindent\z@}

\newcommand{\compose}{\circ}

\endinput

