%% FILE: holmac.tex
%% This is a LaTeX macro for formatting HOL theory generated by format_theory
%%
%% By Wai Wong on 18 July 1990
%%

% Special symbols
\def\sa{$\forall$}
\def\sb{$\lambda$}
\def\sc{$\varepsilon$}
\def\sd{$\iff$}
\def\se{$\exists$}
\def\sg{$\geq$}
\def\sh{$\Rightarrow$}	% `=>`;
\def\si{$\wedge$}
\def\sj{$\mid$}	% `|`;
\def\sk{$\rightarrow$}  % `->`;
\def\sl{$\leq$}
\def\sm{$\supset$}
\def\sn{$\neg$}
\def\so{$\vee$}
\def\sq{{\tt\#}}
\def\sr{$>$}
\def\ss{$\ast$}
\def\st{$\vdash$\ }
\def\su{$\exists$!}
\def\sv{$<$}
\def\sw{\$}
\def\sx{$\backslash$}
\def\sy{\_}
\def\sz{${}^\prime$}

\def\za{\#}
\def\zb{\$}
\def\zc{\%}
\def\zd{\&}
\def\ze{\ast}
\def\zf{<}
\def\zg{\verb"|"}
\def\zh{>}
\def\zi{\[}
\def\zj{$\backslash$}
\def\zk{\]}
\def\zl{\verb|^|}
\def\zm{\_}
\def\zn{\{}
\def\zo{\}}
\def\zp{{\tt\char'176}}

\def\sec#1{\section*{#1}}
\def\thm#1#2{\item[{\tt #1}] \begingroup\obeylines#2\endgroup}
\def\tok#1#2{\item[{\sf #1}]#2}
\def\monthname{\ifcase\month
  \or Jan\or Feb\or Mar\or Apr\or May\or Jun%
  \or Jul\or Aug\or Sep\or Oct\or Nov\or Dec\fi}%
\def\timestring{\begingroup
   \count0 = \time \divide\count0 by 60
   \count2 = \count0 % the hour
   \count4 = \time \multiply\count0 by 60
   \advance\count4 by -\count0 % the minute
   \ifnum\count4<10 \toks1 = {0}% get a leading zero
   \else	    \toks1 = {}%
   \fi
   \ifnum\count2<12 \toks0 = {a.m.}%
   \else	    \toks0 = {p.m.}%
	\advance\count2 by -12
   \fi
   \ifnum\count2=0 \count2 = 12 \fi
   \number\count2:\the\toks1 \number\count4
   \thinspace \the\toks0
\endgroup}%
\def\timestamp{\number\day\space\monthname\space
   \number\year\quad\timestring}%
\def\printtimestamp{Printed at \timestring%
   on \number\day\space\monthname\space\number\year.}

\def\endthy#1{\hbox to\hsize{\hrulefill\ End of theory {\tt#1}\ \hrulefill}}
