% -------------------------------------------------------
% holtexbasic.sty v1.0
%
% For Use with documents generated by EmitTeX.
%
% -------------------------------------------------------

\NeedsTeXFormat{LaTeX2e}
\usepackage{amssymb, makeidx, underscore, fancyvrb}

\fvset{commandchars=\\\{\},xleftmargin=1mm,framesep=1.2mm,fontsize=\small}

\newcommand{\HOLpagestyle}{}
\newcommand{\HOLindex}{\cleardoublepage\printindex}

\newcommand{\HOLDfnTag}[2]{
  \pagebreak[2][\texttt{#2}]\vspace{-1.2mm}
  \index{#1 Theory@\textbf{#1 Theory}!Definitions!#2}}

\newcommand{\HOLThmTag}[2]{
  \pagebreak[2][\texttt{#2}]\vspace{-1.2mm}
  \index{#1 Theory@\textbf{#1 Theory}!Theorems!#2}}

\newcommand{\HOLinline}[1]{\mbox{\textup{\texttt{#1}}}}
\newenvironment{HOLblock}{\begin{alltt}}{\end{alltt}}
\newenvironment{HOLmath}{\begin{displaymath}\begin{array}{l}}{\end{array}\end{displaymath}\ignorespacesafterend}
\newenvironment{HOLarray}{\begin{array}[t]{l}}{\end{array}}

\newcommand{\HOLKeyword}[1]{{\bfseries{\textsf{#1}}}}
\newcommand{\HOLBoundVar}[1]{\ensuremath{\mathit{#1}}}
\newcommand{\HOLFreeVar}[1]{\ensuremath{\mathit{#1}}}
\newcommand{\HOLConst}[1]{\texttt{#1}}
\newcommand{\HOLSymConst}[1]{#1}
\newcommand{\HOLTyOp}[1]{\texttt{#1}}
\newcommand{\HOLStringLit}[1]{\textrm{``#1''}}
\newcommand{\HOLNumLit}[1]{\ensuremath{#1}}
\newcommand{\HOLCharLit}[1]{\textrm{\#``#1''}}
\newcommand{\HOLFieldName}[1]{\textsf{#1}}
\newcommand{\HOLBeginSup}{\begin{math}{}\sp\bgroup\tt}
\newcommand{\HOLBeginSub}{\begin{math}{}\sb\bgroup\tt}
\newcommand{\HOLEndSup}{\egroup\end{math}}
\newcommand{\HOLEndSub}{\egroup\end{math}}
\newcommand{\HOLRuleName}[1]{\textsf{#1}}

\newcommand{\HOLTokenDot}{\ensuremath{.}}
\newcommand{\HOLTokenBackslash}{\texttt{\char'134}}
\newcommand{\HOLTokenTilde}{\texttt{\char'176}}
\newcommand{\HOLTokenDoubleQuote}{\texttt{\char'42}}
\newcommand{\HOLTokenDoublePlus}{\ensuremath{\mathbin{+\mkern-10mu+}}}
\newcommand{\HOLTokenUnderscore}{\texttt{\_}}
\newcommand{\HOLTokenIn}{\ensuremath{\in}}
\newcommand{\HOLTokenNotIn}{\ensuremath{\notin}}
\newcommand{\HOLTokenUnion}{\ensuremath{\cup}}
\newcommand{\HOLTokenRUnion}{\ensuremath{\cup_r}}
\newcommand{\HOLTokenInter}{\ensuremath{\cap}}
\newcommand{\HOLTokenRInter}{\ensuremath{\cap_r}}
\newcommand{\HOLTokenLeftbrace}{\ensuremath{\left\{\right.}}
\newcommand{\HOLTokenRightbrace}{\ensuremath{\left.\right\}}}
\newcommand{\HOLTokenTurnstile}{\ensuremath{\:\:\vdash}}
\newcommand{\HOLTokenLambda}{\ensuremath{\lambda\,}}
\newcommand{\HOLTokenForall}{\ensuremath{\forall\,}}
\newcommand{\HOLTokenExists}{\ensuremath{\exists\,}}
\newcommand{\HOLTokenUnique}{\ensuremath{\exists}!}
\newcommand{\HOLTokenNotEqual}{\ensuremath{\neq}}
\newcommand{\HOLTokenNotEquiv}%
{\ensuremath{\mkern14mu\not\mathrel{\mkern-14mu}\iff}}
\newcommand{\HOLTokenEquiv}{\ensuremath{\iff}}
\newcommand{\HOLTokenMap}{\ensuremath{\rightarrow}}
\newcommand{\HOLTokenLeftmap}{\ensuremath{\leftarrow}}
\newcommand{\HOLTokenImp}{\ensuremath{\Rightarrow}}
\newcommand{\HOLTokenLongmap}{\ensuremath{\longrightarrow}}
\newcommand{\HOLTokenLongimp}{\ensuremath{\Longrightarrow}}
\newcommand{\HOLTokenMapto}{\ensuremath{\mapsto}}
\newcommand{\HOLTokenConj}{\ensuremath{\wedge}}
\newcommand{\HOLTokenDisj}{\ensuremath{\vee}}
\newcommand{\HOLTokenQuote}{\textrm{'}}
\newcommand{\HOLTokenOr}{\ensuremath{\parallel}}
\newcommand{\HOLTokenEor}{\ensuremath{\oplus}}
\newcommand{\HOLTokenNeg}{\ensuremath{\neg}}
\newcommand{\HOLTokenProd}{\ensuremath{\times}}
\newcommand{\HOLTokenLeq}{\ensuremath{\leq}}
\newcommand{\HOLTokenGeq}{\ensuremath{\geq}}
\newcommand{\HOLTokenIsPrefix}{\ensuremath{\preccurlyeq}}
\newcommand{\HOLTokenLo}{\ensuremath{<_+}}
\newcommand{\HOLTokenLs}{\ensuremath{\leq_+}}
\newcommand{\HOLTokenHi}{\ensuremath{>_+}}
\newcommand{\HOLTokenHs}{\ensuremath{\geq_+}}
\newcommand{\HOLTokenLt}{\ensuremath{<}}
\newcommand{\HOLTokenGt}{\ensuremath{>}}
\newcommand{\HOLTokenBar}{\texttt{|}}
\newcommand{\HOLTokenEmpty}{\ensuremath{\emptyset}}
\newcommand{\HOLTokenLeftrec}{\texttt{<|}}
\newcommand{\HOLTokenRightrec}{\texttt{|>}}
\newcommand{\HOLTokenRor}{\ensuremath{\rightleftarrows}}
\newcommand{\HOLTokenRol}{\ensuremath{\leftrightarrows}}
\newcommand{\HOLTokenAsr}{\texttt{>>}}
\newcommand{\HOLTokenLsr}{\texttt{>>>}}
\newcommand{\HOLTokenLsl}{\texttt{<<}}
\newcommand{\HOLTokenSupStar}{\ensuremath{{}^*}}
\newcommand{\HOLTokenSupPlus}{\ensuremath{{}^+}}
\newcommand{\HOLTokenExtract}{\texttt{><}}
\newcommand{\HOLTokenExp}{**}
\newcommand{\HOLTokenLOpenTri}{\ensuremath{\lhd}}
\newcommand{\HOLTokenROpenTri}{\ensuremath{\rhd}}
\newcommand{\HOLTokenLSmallTri}{\ensuremath{\triangleleft}}
\newcommand{\HOLTokenRSmallTri}{\ensuremath{\triangleright}}
\newcommand{\HOLTokenSubset}{\ensuremath{\subseteq}}
\newcommand{\HOLTokenRSubset}{\ensuremath{\subseteq_r}}
\newcommand{\HOLTokenPSubset}{\ensuremath{\subset}}
\newcommand{\HOLTokenSubmap}{\ensuremath{\sqsubseteq}}
\newcommand{\HOLTokenCompose}{\ensuremath{\circ}}
\newcommand{\HOLTokenRCompose}{\ensuremath{\circ_r}}
\newcommand{\HOLTokenInverse}{\ensuremath{{}^{-1}}}
\newcommand{\HOLTokenRInverse}{\ensuremath{{}^T}}
\newcommand{\HOLTokenHilbert}{\ensuremath{\varepsilon}}
\newcommand{\HOLTokenBagLeft}{\ensuremath{\{\!|}}
\newcommand{\HOLTokenBagRight}{\ensuremath{|\!\}}}
\newcommand{\HOLTokenLeftDenote}{\ensuremath{[\hspace{-1pt}|}}
\newcommand{\HOLTokenRightDenote}{\ensuremath{|\hspace{-1pt}]}}
