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