% Inference rule environment with symbolic label and cross-reference.
% Use \begin{inferencerule}{rule-name} ... \end{inferencerule} to define a
% rule.
% Use \ruleref{rule-name} to refer to it.
% The label appears on the left so as to avoid clashing with the side
% conditions on the right.

\makeatletter{}
\def\rulelabel#1{\if@filesw{\let\thepage\relax\xdef\@gtempa{\write\@auxout{\string\newlabel{#1}{{#1}{\thepage}}}}}\@gtempa \fi}
\makeatother{}
\newcommand{\rulefont}{\sc}
\newcommand{\ruleref}[1]{\ifmmode\mbox{\rulefont\ref{#1}}\else{\rulefont\ref{#1}}\fi}

\newenvironment{inferencerule}[1]{\xdef\theinferencerule{#1}\rulelabel{#1}$$}{\eqno\inferencerulename $$}

% For labels on the right:
% The parameter \rulenamewidth should be set to an upper bound on the width of
% a rule name (I don't know any other way to handle the problem of avoiding
% overlap of the name with the rule itself for wide rules!)
\newlength{\rulenamewidth}
\setlength{\rulenamewidth}{.75in}
\newcommand{\inferencerulename}{\hbox to \rulenamewidth{}\llap{\rulefont (\theinferencerule)}}
% labels on the left:
%\newcommand{\inferencerulename}{\hbox to .01pt{}\rlap{\rulefont \hskip -\displaywidth(\theinferencerule)}}


% Type setting inference rules is a real pain.  These macros handle three
% commonly-occurring cases: axioms, plain rules, and rules with stacked
% premises.  It is assumed that we are in display math mode.
% Side conditions are particularly problematic since they usually clash with
% the label.

\newcommand{\axiom}[2]{{\displaystyle\strut #1}\qquad{\displaystyle #2}}

\newcommand{\infrule}[3]{{{\displaystyle\strut #1}\over{\displaystyle\strut #2}}\qquad{\displaystyle #3}}

\newcommand{\stackrule}[4]{%
{\shortstack{$\displaystyle\strut #1$\\$\displaystyle #2$}\over{\displaystyle\strut #3}}\qquad{\displaystyle #4}}

% old macros follow

\comment{
% axiom and inference rule (centered, in math mode,  with name at left)
\newcommand{\axiom}[2]
{\[ \hbox to \columnwidth
    { \rlap{$#2$} \hfil $ #1 $ \hfil }
\]}
\newcommand{\infrule}[4]
{\[ \hbox to \columnwidth
    { \rlap{$#4$} \hfil $
      {{\displaystyle\strut #1}\over{\displaystyle\strut #2}}\quad\makebox[0pt][l]{\it #3} $
      \hfil }
\]}
}

\comment{
% presumed in math mode #1=top, #2=bottom, #3=side condition
\newcommand{\Infrule}[3]{
{{\displaystyle\strut #1}\over{\displaystyle\strut #2}}\quad\makebox[0pt][l]{\it #3}}
% presumed in math mode #1=axiom, #2=side condition
\newcommand{\Axiom}[2]{
{\displaystyle\strut #1}\quad\makebox[0pt][l]{\it #2}}
}
