author | nipkow |
Wed, 26 Aug 1998 16:57:49 +0200 | |
changeset 5375 | 1463e182c533 |
child 5581 | 295bb029170c |
permissions | -rw-r--r-- |
1 \appendix
3 \chapter{Appendix}
4 \label{sec:Appendix}
6 \begin{figure}[htbp]
7 \begin{center}
8 \begin{tabular}{|llll|}
9 \hline
10 \texttt{arities} &
11 \texttt{binder} &
12 \texttt{classes} &
13 \texttt{consts} \\
14 \texttt{default} &
15 \texttt{defs} &
16 \texttt{end} &
17 \texttt{global} \\
18 \texttt{infixl} &
19 \texttt{infixr} &
20 \texttt{instance} &
21 \texttt{local} \\
22 \texttt{mixfix} &
23 \texttt{ML} &
24 \texttt{MLtext} &
25 \texttt{nonterminals} \\
26 \texttt{oracle} &
27 \texttt{output} &
28 \texttt{path} &
29 \texttt{rules} \\
30 \texttt{setup} &
31 \texttt{syntax} &
32 \texttt{translations} &
33 \texttt{types} \\
34 \texttt{constdefs} &
35 \texttt{axclass} &&\\
36 \hline
37 \end{tabular}
38 \end{center}
39 \caption{Keywords in theory files}
40 \label{fig:keywords}
41 \end{figure}
43 \begin{figure}[htbp]
44 \begin{center}
45 \begin{tabular}{|lllll|}
46 \hline
47 \texttt{ALL} &
48 \texttt{case} &
49 \texttt{div} &
50 \texttt{dvd} &
51 \texttt{else} \\
52 \texttt{EX} &
53 \texttt{if} &
54 \texttt{in} &
55 \texttt{INT} &
56 \texttt{Int} \\
57 \texttt{LEAST} &
58 \texttt{let} &
59 \texttt{mod} &
60 \texttt{O} &
61 \texttt{o} \\
62 \texttt{of} &
63 \texttt{op} &
64 \texttt{PROP} &
65 \texttt{SIGMA} &
66 \texttt{then} \\
67 \texttt{Times} &
68 \texttt{UN} &
69 \texttt{Un} &&\\
70 \hline
71 \end{tabular}
72 \end{center}
73 \caption{Reserved words in HOL}
74 \label{fig:ReservedWords}
75 \end{figure}