|
1 \appendix |
|
2 |
|
3 \chapter{Appendix} |
|
4 \label{sec:Appendix} |
|
5 |
|
6 \begin{table}[htbp] |
|
7 \begin{center} |
|
8 \begin{tabular}{|l|l|l|} |
|
9 \hline |
|
10 \indexboldpos{\isasymlbrakk}{$Isabrl} & |
|
11 \texttt{[|}\index{$Isabrl@\ttlbr|bold} & |
|
12 \verb$\<lbrakk>$ \\ |
|
13 \indexboldpos{\isasymrbrakk}{$Isabrr} & |
|
14 \texttt{|]}\index{$Isabrr@\ttrbr|bold} & |
|
15 \verb$\<rbrakk>$ \\ |
|
16 \indexboldpos{\isasymImp}{$IsaImp} & |
|
17 \ttindexboldpos{==>}{$IsaImp} & |
|
18 \verb$\<Longrightarrow>$ \\ |
|
19 \isasymAnd\index{$IsaAnd@\isasymAnd|bold}& |
|
20 \texttt{!!}\index{$IsaAnd@\ttAnd|bold} & |
|
21 \verb$\<And>$ \\ |
|
22 \indexboldpos{\isasymequiv}{$IsaEq} & |
|
23 \ttindexboldpos{==}{$IsaEq} & |
|
24 \verb$\<equiv>$ \\ |
|
25 \indexboldpos{\isasymrightleftharpoons}{$IsaEqTrans} & |
|
26 \ttindexboldpos{==}{$IsaEq} & |
|
27 \verb$\<rightleftharpoons>$ \\ |
|
28 \indexboldpos{\isasymrightharpoonup}{$IsaEqTrans1} & |
|
29 \ttindexboldpos{=>}{$IsaFun} & |
|
30 \verb$\<rightharpoonup>$ \\ |
|
31 \indexboldpos{\isasymleftharpoondown}{$IsaEqTrans2} & |
|
32 \ttindexboldpos{<=}{$IsaFun2} & |
|
33 \verb$\<leftharpoondown>$ \\ |
|
34 \indexboldpos{\isasymlambda}{$Isalam} & |
|
35 \texttt{\%}\indexbold{$Isalam@\texttt{\%}} & |
|
36 \verb$\<lambda>$ \\ |
|
37 \indexboldpos{\isasymFun}{$IsaFun} & |
|
38 \ttindexboldpos{=>}{$IsaFun} & |
|
39 \verb$\<Rightarrow>$ \\ |
|
40 \indexboldpos{\isasymand}{$HOL0and} & |
|
41 \texttt{\&}\indexbold{$HOL0and@{\texttt{\&}}} & |
|
42 \verb$\<and>$ \\ |
|
43 \indexboldpos{\isasymor}{$HOL0or} & |
|
44 \texttt{|}\index{$HOL0or@\ttor|bold} & |
|
45 \verb$\<or>$ \\ |
|
46 \indexboldpos{\isasymimp}{$HOL0imp} & |
|
47 \ttindexboldpos{-->}{$HOL0imp} & |
|
48 \verb$\<longrightarrow>$ \\ |
|
49 \indexboldpos{\isasymnot}{$HOL0not} & |
|
50 \verb$~$\index{$HOL0not@\verb$~$|bold} & |
|
51 \verb$\<not>$ \\ |
|
52 \indexboldpos{\isasymnoteq}{$HOL0noteq} & |
|
53 \verb$~=$\index{$HOL0noteq@\verb$~=$|bold} & |
|
54 \verb$\<noteq>$ \\ |
|
55 \indexboldpos{\isasymforall}{$HOL0All} & |
|
56 \ttindexbold{ALL}, \texttt{!}\index{$HOL0All@\ttall|bold} & |
|
57 \verb$\<forall>$ \\ |
|
58 \indexboldpos{\isasymexists}{$HOL0Ex} & |
|
59 \ttindexbold{EX}, \texttt{?}\index{$HOL0Ex@\texttt{?}|bold} & |
|
60 \verb$\<exists>$ \\ |
|
61 \isasymuniqex\index{$HOL0ExU@\isasymuniqex|bold} & |
|
62 \ttEXU\index{EXX@\ttEXU|bold}, \ttuniquex\index{$HOL0ExU@\ttuniquex|bold} & |
|
63 \verb$\<exists>!$\\ |
|
64 \indexboldpos{\isasymepsilon}{$HOL0ExSome} & |
|
65 \ttindexbold{SOME}, \isa{\at}\index{$HOL2list@\isa{\at}} & |
|
66 \verb$\<epsilon>$\\ |
|
67 \indexboldpos{\isasymcirc}{$HOL1} & |
|
68 \ttindexbold{o} & |
|
69 \verb$\<circ>$\\ |
|
70 \indexboldpos{\isasymbar~\isasymbar}{$HOL2arithfun}& |
|
71 \ttindexbold{abs}& |
|
72 \verb$\<bar> \<bar>$\\ |
|
73 \indexboldpos{\isasymle}{$HOL2arithrel}& |
|
74 \isadxboldpos{<=}{$HOL2arithrel}& |
|
75 \verb$\<le>$\\ |
|
76 \indexboldpos{\isasymtimes}{$Isatype}& |
|
77 \ttindexboldpos{*}{$HOL2arithfun} & |
|
78 \verb$\<times>$\\ |
|
79 \indexboldpos{\isasymin}{$HOL3Set0a}& |
|
80 \ttindexboldpos{:}{$HOL3Set0b} & |
|
81 \verb$\<in>$\\ |
|
82 \isasymnotin\index{$HOL3Set0c@\isasymnotin|bold} & |
|
83 \verb$~:$\index{$HOL3Set0d@\verb$~:$|bold} & |
|
84 \verb$\<notin>$\\ |
|
85 \indexboldpos{\isasymsubseteq}{$HOL3Set0e}& |
|
86 \verb$<=$ & \verb$\<subseteq>$\\ |
|
87 \indexboldpos{\isasymsubset}{$HOL3Set0f}& |
|
88 \verb$<$ & \verb$\<subset>$\\ |
|
89 \indexboldpos{\isasymunion}{$HOL3Set1}& |
|
90 \ttindexbold{Un} & |
|
91 \verb$\<union>$\\ |
|
92 \indexboldpos{\isasyminter}{$HOL3Set1}& |
|
93 \ttindexbold{Int} & |
|
94 \verb$\<inter>$\\ |
|
95 \isasymUnion\index{$HOL3Set2@\isasymUnion|bold}& |
|
96 \ttindexbold{UN}, \ttindexbold{Union} & |
|
97 \verb$\<Union>$\\ |
|
98 \isasymInter\index{$HOL3Set2@\isasymInter|bold}& |
|
99 \ttindexbold{INT}, \ttindexbold{Inter} & |
|
100 \verb$\<Inter>$\\ |
|
101 \isactrlsup{\isacharasterisk}\index{$HOL4star@\isactrlsup{\isacharasterisk}|bold}& |
|
102 \verb$^*$\index{$HOL4star@\verb$^$\texttt{*}|bold} & |
|
103 \verb$\<^sup>*$\\ |
|
104 \isasyminverse\index{$HOL4inv@\isasyminverse|bold}& |
|
105 \verb$^-1$\index{$HOL4inv@\verb$^-1$|bold} & |
|
106 \verb$\<inverse>$\\ |
|
107 \hline |
|
108 \end{tabular} |
|
109 \end{center} |
|
110 \caption{Mathematical Symbols, Their \textsc{ascii}-Equivalents and Internal Names} |
|
111 \label{tab:ascii} |
|
112 \end{table}\indexbold{ASCII@\textsc{ascii} symbols} |
|
113 |
|
114 \input{appendix.tex} |
|
115 |
|
116 \begin{table}[htbp] |
|
117 \begin{center} |
|
118 \begin{tabular}{@{}|lllllllll|@{}} |
|
119 \hline |
|
120 \texttt{ALL} & |
|
121 \texttt{BIT} & |
|
122 \texttt{CHR} & |
|
123 \texttt{EX} & |
|
124 \texttt{GREATEST} & |
|
125 \texttt{INT} & |
|
126 \texttt{Int} & |
|
127 \texttt{LEAST} & |
|
128 \texttt{O} \\ |
|
129 \texttt{OFCLASS} & |
|
130 \texttt{PI} & |
|
131 \texttt{PROP} & |
|
132 \texttt{SIGMA} & |
|
133 \texttt{SOME} & |
|
134 \texttt{THE} & |
|
135 \texttt{TYPE} & |
|
136 \texttt{UN} & |
|
137 \texttt{Un} \\ |
|
138 \texttt{WRT} & |
|
139 \texttt{case} & |
|
140 \texttt{choose} & |
|
141 \texttt{div} & |
|
142 \texttt{dvd} & |
|
143 \texttt{else} & |
|
144 \texttt{funcset} & |
|
145 \texttt{if} & |
|
146 \texttt{in} \\ |
|
147 \texttt{let} & |
|
148 \texttt{mem} & |
|
149 \texttt{mod} & |
|
150 \texttt{o} & |
|
151 \texttt{of} & |
|
152 \texttt{op} & |
|
153 \texttt{then} &&\\ |
|
154 \hline |
|
155 \end{tabular} |
|
156 \end{center} |
|
157 \caption{Reserved Words in HOL Terms} |
|
158 \label{tab:ReservedWords} |
|
159 \end{table} |
|
160 |
|
161 |
|
162 %\begin{table}[htbp] |
|
163 %\begin{center} |
|
164 %\begin{tabular}{|lllll|} |
|
165 %\hline |
|
166 %\texttt{and} & |
|
167 %\texttt{binder} & |
|
168 %\texttt{concl} & |
|
169 %\texttt{congs} \\ |
|
170 %\texttt{distinct} & |
|
171 %\texttt{files} & |
|
172 %\texttt{in} & |
|
173 %\texttt{induction} & |
|
174 %\texttt{infixl} \\ |
|
175 %\texttt{infixr} & |
|
176 %\texttt{inject} & |
|
177 %\texttt{intrs} & |
|
178 %\texttt{is} & |
|
179 %\texttt{monos} \\ |
|
180 %\texttt{output} & |
|
181 %\texttt{where} & |
|
182 % & |
|
183 % & |
|
184 % \\ |
|
185 %\hline |
|
186 %\end{tabular} |
|
187 %\end{center} |
|
188 %\caption{Minor Keywords in HOL Theories} |
|
189 %\label{tab:keywords} |
|
190 %\end{table} |