1% ------------------------------------------------------- 2% holtexbasic.sty v1.0 3% 4% For Use with documents generated by EmitTeX. 5% 6% ------------------------------------------------------- 7 8\NeedsTeXFormat{LaTeX2e} 9\usepackage{amssymb, underscore, fancyvrb, amsmath} 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{\HOLStringLitDG}[1]{\textrm{\guillemotleft#1\guillemotright}} 37\newcommand{\HOLStringLitSG}[1]{\textrm{\guilsinglleft#1\guilsinglright}} 38\newcommand{\HOLNumLit}[1]{\ensuremath{#1}} 39\newcommand{\HOLCharLit}[1]{\textrm{\#``#1''}} 40\newcommand{\HOLFieldName}[1]{\textsf{#1}} 41\newcommand{\HOLBeginSup}{\begin{math}{}\sp\bgroup\tt} 42\newcommand{\HOLBeginSub}{\begin{math}{}\sb\bgroup\tt} 43\newcommand{\HOLEndSup}{\egroup\end{math}} 44\newcommand{\HOLEndSub}{\egroup\end{math}} 45\newcommand{\HOLRuleName}[1]{\textsf{#1}} 46 47\newcommand{\HOLTokenDot}{\ensuremath{.}} 48\newcommand{\HOLTokenBackslash}{\texttt{\char'134}} 49\newcommand{\HOLTokenTilde}{\texttt{\char'176}} 50\newcommand{\HOLTokenDoubleQuote}{\texttt{\char'42}} 51\newcommand{\HOLTokenDoublePlus}{\ensuremath{\mathbin{+\mkern-10mu+}}} 52\newcommand{\HOLTokenUnderscore}{\texttt{\_}} 53\newcommand{\HOLTokenIn}{\ensuremath{\in}} 54\newcommand{\HOLTokenNotIn}{\ensuremath{\notin}} 55\newcommand{\HOLTokenUnion}{\ensuremath{\cup}} 56\newcommand{\HOLTokenBigUnion}{\ensuremath{\bigcup}} 57\newcommand{\HOLTokenRUnion}{\ensuremath{\cup_r}} 58\newcommand{\HOLTokenInter}{\ensuremath{\cap}} 59\newcommand{\HOLTokenBigInter}{\ensuremath{\bigcap}} 60\newcommand{\HOLTokenRInter}{\ensuremath{\cap_r}} 61\newcommand{\HOLTokenLeftbrace}{\ensuremath{\left\{\right.}} 62\newcommand{\HOLTokenRightbrace}{\ensuremath{\left.\right\}}} 63\newcommand{\HOLTokenTurnstile}{\ensuremath{\:\:\vdash}} 64\newcommand{\HOLTokenLambda}{\ensuremath{\lambda\,}} 65\newcommand{\HOLTokenForall}{\ensuremath{\forall\,}} 66\newcommand{\HOLTokenExists}{\ensuremath{\exists\,}} 67\newcommand{\HOLTokenUnique}{\ensuremath{\exists}!} 68\newcommand{\HOLTokenNotEqual}{\ensuremath{\neq}} 69\newcommand{\HOLTokenNotEquiv}% 70{\ensuremath{\mkern14mu\not\mathrel{\mkern-14mu}\iff}} 71\newcommand{\HOLTokenEquiv}{\ensuremath{\iff}} 72\newcommand{\HOLTokenMap}{\ensuremath{\rightarrow}} 73\newcommand{\HOLTokenLeftmap}{\ensuremath{\leftarrow}} 74\newcommand{\HOLTokenImp}{\ensuremath{\Rightarrow}} 75\newcommand{\HOLTokenLongmap}{\ensuremath{\longrightarrow}} 76\newcommand{\HOLTokenLongimp}{\ensuremath{\Longrightarrow}} 77\newcommand{\HOLTokenMapto}{\ensuremath{\mapsto}} 78\newcommand{\HOLTokenConj}{\ensuremath{\wedge}} 79\newcommand{\HOLTokenDisj}{\ensuremath{\vee}} 80\newcommand{\HOLTokenQuote}{\textrm{'}} 81\newcommand{\HOLTokenOr}{\ensuremath{\parallel}} 82\newcommand{\HOLTokenEor}{\ensuremath{\oplus}} 83\newcommand{\HOLTokenNeg}{\ensuremath{\neg}} 84\newcommand{\HOLTokenProd}{\ensuremath{\times}} 85\newcommand{\HOLTokenLeq}{\ensuremath{\leq}} 86\newcommand{\HOLTokenGeq}{\ensuremath{\geq}} 87\newcommand{\HOLTokenIsPrefix}{\ensuremath{\preccurlyeq}} 88\newcommand{\HOLTokenLo}{\ensuremath{<_+}} 89\newcommand{\HOLTokenLs}{\ensuremath{\leq_+}} 90\newcommand{\HOLTokenHi}{\ensuremath{>_+}} 91\newcommand{\HOLTokenHs}{\ensuremath{\geq_+}} 92\newcommand{\HOLTokenLt}{\ensuremath{<}} 93\newcommand{\HOLTokenGt}{\ensuremath{>}} 94\newcommand{\HOLTokenBar}{\texttt{|}} 95\newcommand{\HOLTokenEmpty}{\ensuremath{\emptyset}} 96\newcommand{\HOLTokenLeftrec}{\texttt{<|}} 97\newcommand{\HOLTokenRightrec}{\texttt{|>}} 98\newcommand{\HOLTokenRor}{\ensuremath{\rightleftarrows}} 99\newcommand{\HOLTokenRol}{\ensuremath{\leftrightarrows}} 100\newcommand{\HOLTokenAsr}{\ensuremath{\gg}} %{\texttt{>>}} 101\newcommand{\HOLTokenLsr}{\ensuremath{\ggg}} % {\texttt{>>>}} 102\newcommand{\HOLTokenLsl}{\ensuremath{\ll}} % {\texttt{<<}} 103\newcommand{\HOLTokenSupStar}{\ensuremath{{}^*}} 104\newcommand{\HOLTokenSupPlus}{\ensuremath{{}^+}} 105\newcommand{\HOLTokenSupTwo}{\ensuremath{{}^2}} 106\newcommand{\HOLTokenSupThree}{\ensuremath{{}^3}} 107\newcommand{\HOLTokenSupFour}{\ensuremath{{}^4}} 108\newcommand{\HOLTokenExtract}{\texttt{><}} 109\newcommand{\HOLTokenExp}{**} 110\newcommand{\HOLTokenLOpenTri}{\ensuremath{\lhd}} 111\newcommand{\HOLTokenROpenTri}{\ensuremath{\rhd}} 112\newcommand{\HOLTokenLSmallTri}{\ensuremath{\triangleleft}} 113\newcommand{\HOLTokenRSmallTri}{\ensuremath{\triangleright}} 114\newcommand{\HOLTokenSubset}{\ensuremath{\subseteq}} 115\newcommand{\HOLTokenRSubset}{\ensuremath{\subseteq_r}} 116\newcommand{\HOLTokenPSubset}{\ensuremath{\subset}} 117\newcommand{\HOLTokenSubmap}{\ensuremath{\sqsubseteq}} 118\newcommand{\HOLTokenCompose}{\ensuremath{\circ}} 119\newcommand{\HOLTokenRCompose}{\ensuremath{\circ_r}} 120\newcommand{\HOLTokenInverse}{\ensuremath{{}^{-1}}} 121\newcommand{\HOLTokenRInverse}{\ensuremath{{}^T}} 122\newcommand{\HOLTokenHilbert}{\ensuremath{\varepsilon}} 123\newcommand{\HOLTokenBagLeft}{\ensuremath{\{\!|}} 124\newcommand{\HOLTokenBagRight}{\ensuremath{|\!\}}} 125\newcommand{\HOLTokenLeftDenote}{\ensuremath{[\hspace{-1pt}|}} 126\newcommand{\HOLTokenRightDenote}{\ensuremath{|\hspace{-1pt}]}} 127\newcommand{\HOLTokenDefEquality}{\ensuremath{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\tiny\sffamily def}}}{=}}}} 128\newcommand{\HOLTokenSum}{\ensuremath{\sum}} 129\newcommand{\HOLTokenPI}{\ensuremath{\prod}} % \HOLTokenProd is already defined 130\newcommand{\HOLTokenOne}{\ensuremath{\mathbbm{1}}} 131\newcommand{\HOLTokenIntegral}{\ensuremath{\int}} 132\newcommand{\HOLTokenIntegralPlus}{\ensuremath{\int^{+}}} 133