1% ------------------------------------------------------- 2% holtexbasic.sty v1.0 3% 4% For Use with documents generated by EmitTeX. 5% 6% ------------------------------------------------------- 7 8\NeedsTeXFormat{LaTeX2e} 9\usepackage{amssymb, makeidx, underscore, fancyvrb} 10 11\fvset{commandchars=\\\{\},xleftmargin=1mm,framesep=1.2mm,fontsize=\small} 12 13\newcommand{\HOLpagestyle}{} 14\newcommand{\HOLindex}{\cleardoublepage\printindex} 15 16\newcommand{\HOLDfnTag}[2]{ 17 \pagebreak[2][\texttt{#2}]\vspace{-1.2mm} 18 \index{#1 Theory@\textbf{#1 Theory}!Definitions!#2}} 19 20\newcommand{\HOLThmTag}[2]{ 21 \pagebreak[2][\texttt{#2}]\vspace{-1.2mm} 22 \index{#1 Theory@\textbf{#1 Theory}!Theorems!#2}} 23 24\newcommand{\HOLinline}[1]{\mbox{\textup{\texttt{#1}}}} 25\newenvironment{HOLblock}{\begin{alltt}}{\end{alltt}} 26\newenvironment{HOLmath}{\begin{displaymath}\begin{array}{l}}{\end{array}\end{displaymath}\ignorespacesafterend} 27\newenvironment{HOLarray}{\begin{array}[t]{l}}{\end{array}} 28 29\newcommand{\HOLKeyword}[1]{{\bfseries{\textsf{#1}}}} 30\newcommand{\HOLBoundVar}[1]{\ensuremath{\mathit{#1}}} 31\newcommand{\HOLFreeVar}[1]{\ensuremath{\mathit{#1}}} 32\newcommand{\HOLConst}[1]{\texttt{#1}} 33\newcommand{\HOLSymConst}[1]{#1} 34\newcommand{\HOLTyOp}[1]{\texttt{#1}} 35\newcommand{\HOLStringLit}[1]{\textrm{``#1''}} 36\newcommand{\HOLNumLit}[1]{\ensuremath{#1}} 37\newcommand{\HOLCharLit}[1]{\textrm{\#``#1''}} 38\newcommand{\HOLFieldName}[1]{\textsf{#1}} 39\newcommand{\HOLBeginSup}{\begin{math}{}\sp\bgroup\tt} 40\newcommand{\HOLBeginSub}{\begin{math}{}\sb\bgroup\tt} 41\newcommand{\HOLEndSup}{\egroup\end{math}} 42\newcommand{\HOLEndSub}{\egroup\end{math}} 43\newcommand{\HOLRuleName}[1]{\textsf{#1}} 44 45\newcommand{\HOLTokenDot}{\ensuremath{.}} 46\newcommand{\HOLTokenBackslash}{\texttt{\char'134}} 47\newcommand{\HOLTokenTilde}{\texttt{\char'176}} 48\newcommand{\HOLTokenDoubleQuote}{\texttt{\char'42}} 49\newcommand{\HOLTokenDoublePlus}{\ensuremath{\mathbin{+\mkern-10mu+}}} 50\newcommand{\HOLTokenUnderscore}{\texttt{\_}} 51\newcommand{\HOLTokenIn}{\ensuremath{\in}} 52\newcommand{\HOLTokenNotIn}{\ensuremath{\notin}} 53\newcommand{\HOLTokenUnion}{\ensuremath{\cup}} 54\newcommand{\HOLTokenRUnion}{\ensuremath{\cup_r}} 55\newcommand{\HOLTokenInter}{\ensuremath{\cap}} 56\newcommand{\HOLTokenRInter}{\ensuremath{\cap_r}} 57\newcommand{\HOLTokenLeftbrace}{\ensuremath{\left\{\right.}} 58\newcommand{\HOLTokenRightbrace}{\ensuremath{\left.\right\}}} 59\newcommand{\HOLTokenTurnstile}{\ensuremath{\:\:\vdash}} 60\newcommand{\HOLTokenLambda}{\ensuremath{\lambda\,}} 61\newcommand{\HOLTokenForall}{\ensuremath{\forall\,}} 62\newcommand{\HOLTokenExists}{\ensuremath{\exists\,}} 63\newcommand{\HOLTokenUnique}{\ensuremath{\exists}!} 64\newcommand{\HOLTokenNotEqual}{\ensuremath{\neq}} 65\newcommand{\HOLTokenNotEquiv}% 66{\ensuremath{\mkern14mu\not\mathrel{\mkern-14mu}\iff}} 67\newcommand{\HOLTokenEquiv}{\ensuremath{\iff}} 68\newcommand{\HOLTokenMap}{\ensuremath{\rightarrow}} 69\newcommand{\HOLTokenLeftmap}{\ensuremath{\leftarrow}} 70\newcommand{\HOLTokenImp}{\ensuremath{\Rightarrow}} 71\newcommand{\HOLTokenLongmap}{\ensuremath{\longrightarrow}} 72\newcommand{\HOLTokenLongimp}{\ensuremath{\Longrightarrow}} 73\newcommand{\HOLTokenMapto}{\ensuremath{\mapsto}} 74\newcommand{\HOLTokenConj}{\ensuremath{\wedge}} 75\newcommand{\HOLTokenDisj}{\ensuremath{\vee}} 76\newcommand{\HOLTokenQuote}{\textrm{'}} 77\newcommand{\HOLTokenOr}{\ensuremath{\parallel}} 78\newcommand{\HOLTokenEor}{\ensuremath{\oplus}} 79\newcommand{\HOLTokenNeg}{\ensuremath{\neg}} 80\newcommand{\HOLTokenProd}{\ensuremath{\times}} 81\newcommand{\HOLTokenLeq}{\ensuremath{\leq}} 82\newcommand{\HOLTokenGeq}{\ensuremath{\geq}} 83\newcommand{\HOLTokenIsPrefix}{\ensuremath{\preccurlyeq}} 84\newcommand{\HOLTokenLo}{\ensuremath{<_+}} 85\newcommand{\HOLTokenLs}{\ensuremath{\leq_+}} 86\newcommand{\HOLTokenHi}{\ensuremath{>_+}} 87\newcommand{\HOLTokenHs}{\ensuremath{\geq_+}} 88\newcommand{\HOLTokenLt}{\ensuremath{<}} 89\newcommand{\HOLTokenGt}{\ensuremath{>}} 90\newcommand{\HOLTokenBar}{\texttt{|}} 91\newcommand{\HOLTokenEmpty}{\ensuremath{\emptyset}} 92\newcommand{\HOLTokenLeftrec}{\texttt{<|}} 93\newcommand{\HOLTokenRightrec}{\texttt{|>}} 94\newcommand{\HOLTokenRor}{\ensuremath{\rightleftarrows}} 95\newcommand{\HOLTokenRol}{\ensuremath{\leftrightarrows}} 96\newcommand{\HOLTokenAsr}{\texttt{>>}} 97\newcommand{\HOLTokenLsr}{\texttt{>>>}} 98\newcommand{\HOLTokenLsl}{\texttt{<<}} 99\newcommand{\HOLTokenSupStar}{\ensuremath{{}^*}} 100\newcommand{\HOLTokenSupPlus}{\ensuremath{{}^+}} 101\newcommand{\HOLTokenExtract}{\texttt{><}} 102\newcommand{\HOLTokenExp}{**} 103\newcommand{\HOLTokenLOpenTri}{\ensuremath{\lhd}} 104\newcommand{\HOLTokenROpenTri}{\ensuremath{\rhd}} 105\newcommand{\HOLTokenLSmallTri}{\ensuremath{\triangleleft}} 106\newcommand{\HOLTokenRSmallTri}{\ensuremath{\triangleright}} 107\newcommand{\HOLTokenSubset}{\ensuremath{\subseteq}} 108\newcommand{\HOLTokenRSubset}{\ensuremath{\subseteq_r}} 109\newcommand{\HOLTokenPSubset}{\ensuremath{\subset}} 110\newcommand{\HOLTokenSubmap}{\ensuremath{\sqsubseteq}} 111\newcommand{\HOLTokenCompose}{\ensuremath{\circ}} 112\newcommand{\HOLTokenRCompose}{\ensuremath{\circ_r}} 113\newcommand{\HOLTokenInverse}{\ensuremath{{}^{-1}}} 114\newcommand{\HOLTokenRInverse}{\ensuremath{{}^T}} 115\newcommand{\HOLTokenHilbert}{\ensuremath{\varepsilon}} 116\newcommand{\HOLTokenBagLeft}{\ensuremath{\{\!|}} 117\newcommand{\HOLTokenBagRight}{\ensuremath{|\!\}}} 118\newcommand{\HOLTokenLeftDenote}{\ensuremath{[\hspace{-1pt}|}} 119\newcommand{\HOLTokenRightDenote}{\ensuremath{|\hspace{-1pt}]}} 120