\def\trule#1{\hbox{\vbox to 3mm{\vfill\hrule height0.4pt width#1\vskip2pt\hrule height0.4pt width#1\vfill}}}

\def\rrule#1{\hbox{\vbox to 3mm{\vfill\hrule height0.4pt width#1\vfill}}}


\def\Rule#1#2{\mbox{${\displaystyle\raise 3pt\hbox{$\;\;\;#1\;\;\;$}}
                          \over
                     {\displaystyle\lower5pt\hbox{$\;\;\;#2\;\;\;$}}$}}


% ---------------------------------------------------------------------
% Macros for little HOL sessions displayed in boxes.
%
% Usage: (1) \setcounter{sessioncount}{1} resets the session counter
%
%	 (2) \begin{session}\begin{verbatim}
%	      .
%	       < lines from hol session >
%	      .
%	     \end{verbatim}\end{session}
%
%            typesets the session in a numbered box.
% ---------------------------------------------------------------------

\newlength{\hsbw}
\setlength{\hsbw}{83mm}
\addtolength{\hsbw}{-\arrayrulewidth}
\addtolength{\hsbw}{-\tabcolsep}
\newcommand\HOLSpacing{12pt}

\newcounter{sessioncount}
\setcounter{sessioncount}{1}

\newenvironment{session}{\begin{flushleft}
 \begin{tabular}{@{}|c@{}|@{}}\hline
 \begin{minipage}[b]{\hsbw}
% \vspace*{-.5pt}
 \begin{flushright}
 \rule{0.01in}{.15in}\rule{0.3in}{0.01in}\hspace{-0.35in}
 \raisebox{0.04in}{\makebox[0.3in][c]{\footnotesize\sl \thesessioncount}}
 \end{flushright}
 \vspace*{-11.5mm}
 \begingroup}{\endgroup\end{minipage}\\ \hline
 \end{tabular}
 \end{flushleft}
 \stepcounter{sessioncount}}