| author | wenzelm |
| Tue, 09 May 2000 15:10:25 +0200 | |
| changeset 8845 | 03a2ae3059da |
| parent 8771 | 026f37a86ea7 |
| child 9541 | d17c0b34d5c8 |
| permissions | -rw-r--r-- |
1 \appendix
3 \chapter{Appendix}
4 \label{sec:Appendix}
6 \begin{figure}[htbp]
7 \begin{center}
8 \begin{tabular}{|ccccccccccc|}
9 \hline
10 \indexboldpos{\isasymand}{$HOL0and} &
11 \indexboldpos{\isasymor}{$HOL0or} &
12 \indexboldpos{\isasymimp}{$HOL0imp} &
13 \indexboldpos{\isasymnot}{$HOL0not} &
14 \indexboldpos{\isasymnoteq}{$HOL0noteq} &
15 \indexboldpos{\isasymforall}{$HOL0All} &
16 \isasymforall &
17 \indexboldpos{\isasymexists}{$HOL0Ex} &
18 \isasymexists &
19 \isasymuniqex\index{$HOL0ExU@\isasymuniqex|bold} &
20 \isasymuniqex \\
21 \texttt{\&}\indexbold{$HOL0and@{\texttt{\&}}} &
22 \texttt{|}\index{$HOL0or@\ttor|bold} &
23 \ttindexboldpos{-->}{$HOL0imp} &
24 \verb$~$\index{$HOL0not@\verb$~$|bold} &
25 \verb$~=$\index{$HOL0noteq@\verb$~=$|bold} &
26 \ttindexbold{ALL} &
27 \texttt{!}\index{$HOL0All@\ttall|bold} &
28 \ttindexbold{EX} &
29 \texttt{?}\index{$HOL0Ex@\texttt{?}|bold} &
30 \ttEXU\index{EXX@\ttEXU|bold} &
31 \ttuniquex\index{$HOL0ExU@\ttuniquex|bold}\\
32 \hline\hline
33 \indexboldpos{\isasymlbrakk}{$Isabrl} &
34 \indexboldpos{\isasymrbrakk}{$Isabrr} &
35 \indexboldpos{\isasymImp}{$IsaImp} &
36 \indexboldpos{\isasymAnd}{$IsaAnd} &
37 \indexboldpos{\isasymequiv}{$IsaEq} &
38 \indexboldpos{\isasymlambda}{$Isalam} &
39 \indexboldpos{\isasymFun}{$IsaFun}&
40 &
41 &
42 &
43 \\
44 \texttt{[|}\index{$Isabrl@\ttlbr|bold} &
45 \texttt{|]}\index{$Isabrr@\ttrbr|bold} &
46 \ttindexboldpos{==>}{$IsaImp} &
47 \texttt{!!}\index{$IsaAnd@\ttAnd|bold} &
48 \ttindexboldpos{==}{$IsaEq} &
49 \texttt{\%}\indexbold{$Isalam@\texttt{\%}} &
50 \ttindexboldpos{=>}{$IsaFun}&
51 &
52 &
53 &
54 \\
55 \hline\hline
56 \indexboldpos{\isasymcirc}{$HOL1} &
57 \indexboldpos{\isasymle}{$HOL2arithrel}&
58 &
59 &
60 &
61 &
62 &
63 &
64 &
65 &
66 \\
67 \ttindexbold{o} &
68 \ttindexboldpos{<=}{$HOL2arithrel}&
69 &
70 &
71 &
72 &
73 &
74 &
75 &
76 &
77 \\
78 \hline
79 \end{tabular}
80 \end{center}
81 \caption{Mathematical symbols and their ASCII-equivalents}
82 \label{fig:ascii}
83 \end{figure}\indexbold{ASCII symbols}
86 \begin{figure}[htbp]
87 \begin{center}
88 \begin{tabular}{|lllll|}
89 \hline
90 \texttt{ALL} &
91 \texttt{case} &
92 \texttt{div} &
93 \texttt{dvd} &
94 \texttt{else} \\
95 \texttt{EX} &
96 \texttt{if} &
97 \texttt{in} &
98 \texttt{INT} &
99 \texttt{Int} \\
100 \texttt{LEAST} &
101 \texttt{let} &
102 \texttt{mod} &
103 \texttt{O} &
104 \texttt{o} \\
105 \texttt{of} &
106 \texttt{op} &
107 \texttt{PROP} &
108 \texttt{SIGMA} &
109 \texttt{then} \\
110 \texttt{Times} &
111 \texttt{UN} &
112 \texttt{Un} &&\\
113 \hline
114 \end{tabular}
115 \end{center}
116 \caption{Reserved words in HOL terms}
117 \label{fig:ReservedWords}
118 \end{figure}
121 \begin{figure}[htbp]
123 %FIXME too long to be useful!??
124 \begin{center}
125 \begin{tabular}{|lll|}
126 \hline
127 \texttt{ML} &
128 \texttt{ML_command} &
129 \texttt{ML_setup} \\
130 \texttt{also} &
131 \texttt{apply} &
132 \texttt{apply_end} \\
133 \texttt{arities} &
134 \texttt{assume} &
135 \texttt{axclass} \\
136 \texttt{axioms} &
137 \texttt{back} &
138 \texttt{by} \\
139 \texttt{cannot_undo} &
140 \texttt{case} &
141 \texttt{cd} \\
142 \texttt{chapter} &
143 \texttt{classes} &
144 \texttt{classrel} \\
145 \texttt{clear_undos} &
146 \texttt{coinductive} &
147 \texttt{commit} \\
148 \texttt{constdefs} &
149 \texttt{consts} &
150 \texttt{context} \\
151 \texttt{datatype} &
152 \texttt{def} &
153 \texttt{defaultsort} \\
154 \texttt{defer} &
155 \texttt{defer_recdef} &
156 \texttt{defs} \\
157 \texttt{disable_pr} &
158 \texttt{enable_pr} &
159 \texttt{end} \\
160 \texttt{exit} &
161 \texttt{finally} &
162 \texttt{fix} \\
163 \texttt{from} &
164 \texttt{global} &
165 \texttt{have} \\
166 \texttt{header} &
167 \texttt{help} &
168 \texttt{hence} \\
169 \texttt{hide} &
170 \texttt{inductive} &
171 \texttt{inductive_cases} \\
172 \texttt{init_toplevel} &
173 \texttt{instance} &
174 \texttt{judgment} \\
175 \texttt{kill} &
176 \texttt{kill_thy} &
177 \texttt{lemma} \\
178 \texttt{lemmas} &
179 \texttt{let} &
180 \texttt{local} \\
181 \texttt{moreover} &
182 \texttt{next} &
183 \texttt{nonterminals} \\
184 \texttt{note} &
185 \texttt{obtain} &
186 \texttt{oops} \\
187 \texttt{oracle} &
188 \texttt{parse_ast_translation} &
189 \texttt{parse_translation} \\
190 \texttt{pr} &
191 \texttt{prefer} &
192 \texttt{presume} \\
193 \texttt{pretty_setmargin} &
194 \texttt{primrec} &
195 \texttt{print_ast_translation} \\
196 \texttt{print_attributes} &
197 \texttt{print_binds} &
198 \texttt{print_cases} \\
199 \texttt{print_claset} &
200 \texttt{print_context} &
201 \texttt{print_facts} \\
202 \texttt{print_methods} &
203 \texttt{print_simpset} &
204 \texttt{print_syntax} \\
205 \texttt{print_theorems} &
206 \texttt{print_theory} &
207 \texttt{print_translation} \\
208 \texttt{proof} &
209 \texttt{prop} &
210 \texttt{pwd} \\
211 \texttt{qed} &
212 \texttt{quit} &
213 \texttt{recdef} \\
214 \texttt{record} &
215 \texttt{redo} &
216 \texttt{remove_thy} \\
217 \texttt{rep_datatype} &
218 \texttt{sect} &
219 \texttt{section} \\
220 \texttt{setup} &
221 \texttt{show} &
222 \texttt{sorry} \\
223 \texttt{subsect} &
224 \texttt{subsection} &
225 \texttt{subsubsect} \\
226 \texttt{subsubsection} &
227 \texttt{syntax} &
228 \texttt{term} \\
229 \texttt{text} &
230 \texttt{text_raw} &
231 \texttt{then} \\
232 \texttt{theorem} &
233 \texttt{theorems} &
234 \texttt{theory} \\
235 \texttt{thm} &
236 \texttt{thms_containing} &
237 \texttt{thus} \\
238 \texttt{token_translation} &
239 \texttt{touch_all_thys} &
240 \texttt{touch_child_thys} \\
241 \texttt{touch_thy} &
242 \texttt{translations} &
243 \texttt{txt} \\
244 \texttt{txt_raw} &
245 \texttt{typ} &
246 \texttt{typed_print_translation} \\
247 \texttt{typedecl} &
248 \texttt{typedef} &
249 \texttt{types} \\
250 \texttt{ultimately} &
251 \texttt{undo} &
252 \texttt{undos_proof} \\
253 \texttt{update_thy} &
254 \texttt{update_thy_only} &
255 \texttt{use} \\
256 \texttt{use_thy} &
257 \texttt{use_thy_only} &
258 \texttt{welcome} \\
259 \texttt{with} &
260 &
261 \\
262 \hline
263 \end{tabular}
264 \end{center}
266 \begin{center}
267 \begin{tabular}{|lllll|}
268 \hline
269 \texttt{and} &
270 \texttt{binder} &
271 \texttt{con_defs} &
272 \texttt{concl} &
273 \texttt{congs} \\
274 \texttt{distinct} &
275 \texttt{files} &
276 \texttt{in} &
277 \texttt{induction} &
278 \texttt{infixl} \\
279 \texttt{infixr} &
280 \texttt{inject} &
281 \texttt{intrs} &
282 \texttt{is} &
283 \texttt{monos} \\
284 \texttt{output} &
285 \texttt{where} &
286 &
287 &
288 \\
289 \hline
290 \end{tabular}
291 \end{center}
294 \caption{Commands and minor keywords in HOL theories}
295 \label{fig:keywords}
296 \end{figure}