-
Notifications
You must be signed in to change notification settings - Fork 0
/
holtexbasic.sty
122 lines (114 loc) · 5.53 KB
/
holtexbasic.sty
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
% -------------------------------------------------------
% holtexbasic.sty v1.0
%
% For Use with documents generated by EmitTeX.
%
% -------------------------------------------------------
\NeedsTeXFormat{LaTeX2e}
\usepackage{underscore, fancyvrb, amsmath}
\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]{{\text{\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{\HOLStringLitDG}[1]{\textrm{\guillemotleft#1\guillemotright}}
\newcommand{\HOLStringLitSG}[1]{\textrm{\guilsinglleft#1\guilsinglright}}
\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}]}}
\newcommand{\HOLTokenDefEquality}{\ensuremath{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\tiny\sffamily def}}}{=}}}}