1\def\trule#1{\hbox{\vbox to 3mm{\vfill\hrule height0.4pt width#1\vskip2pt\hrule height0.4pt width#1\vfill}}}
2
3\def\rrule#1{\hbox{\vbox to 3mm{\vfill\hrule height0.4pt width#1\vfill}}}
4
5
6\def\Rule#1#2{\mbox{${\displaystyle\raise 3pt\hbox{$\;\;\;#1\;\;\;$}}
7                          \over
8                     {\displaystyle\lower5pt\hbox{$\;\;\;#2\;\;\;$}}$}}
9
10
11% ---------------------------------------------------------------------
12% Macros for little HOL sessions displayed in boxes.
13%
14% Usage: (1) \setcounter{sessioncount}{1} resets the session counter
15%
16%	 (2) \begin{session}\begin{verbatim}
17%	      .
18%	       < lines from hol session >
19%	      .
20%	     \end{verbatim}\end{session}
21%
22%            typesets the session in a numbered box.
23% ---------------------------------------------------------------------
24
25\newlength{\hsbw}
26\setlength{\hsbw}{83mm}
27\addtolength{\hsbw}{-\arrayrulewidth}
28\addtolength{\hsbw}{-\tabcolsep}
29\newcommand\HOLSpacing{12pt}
30
31\newcounter{sessioncount}
32\setcounter{sessioncount}{1}
33
34\newenvironment{session}{\begin{flushleft}
35 \begin{tabular}{@{}|c@{}|@{}}\hline
36 \begin{minipage}[b]{\hsbw}
37% \vspace*{-.5pt}
38 \begin{flushright}
39 \rule{0.01in}{.15in}\rule{0.3in}{0.01in}\hspace{-0.35in}
40 \raisebox{0.04in}{\makebox[0.3in][c]{\footnotesize\sl \thesessioncount}}
41 \end{flushright}
42 \vspace*{-11.5mm}
43 \begingroup}{\endgroup\end{minipage}\\ \hline
44 \end{tabular}
45 \end{flushleft}
46 \stepcounter{sessioncount}}
47
48