equal
deleted
inserted
replaced
1 \appendix |
|
2 |
|
3 \chapter{Appendix} |
|
4 \label{sec:Appendix} |
|
5 |
|
6 \begin{figure}[htbp] |
|
7 \begin{center} |
|
8 \begin{tabular}{|lllll|} |
|
9 \hline |
|
10 \texttt{and} & |
|
11 \texttt{arities} & |
|
12 \texttt{assumes} & |
|
13 \texttt{axclass} & |
|
14 \texttt{binder} \\ |
|
15 \texttt{classes} & |
|
16 \texttt{constdefs} & |
|
17 \texttt{consts} & |
|
18 \texttt{default} & |
|
19 \texttt{defines} \\ |
|
20 \texttt{defs} & |
|
21 \texttt{end} & |
|
22 \texttt{fixes} & |
|
23 \texttt{global} & |
|
24 \texttt{inductive} \\ |
|
25 \texttt{infixl} & |
|
26 \texttt{infixr} & |
|
27 \texttt{instance} & |
|
28 \texttt{local} & |
|
29 \texttt{locale} \\ |
|
30 \texttt{mixfix} & |
|
31 \texttt{ML} & |
|
32 \texttt{MLtext} & |
|
33 \texttt{nonterminals} & |
|
34 \texttt{oracle} \\ |
|
35 \texttt{output} & |
|
36 \texttt{path} & |
|
37 \texttt{primrec} & |
|
38 \texttt{rules} & |
|
39 \texttt{setup} \\ |
|
40 \texttt{syntax} & |
|
41 \texttt{translations} & |
|
42 \texttt{typedef} & |
|
43 \texttt{types} &\\ |
|
44 \hline |
|
45 \end{tabular} |
|
46 \end{center} |
|
47 \caption{Keywords in theory files} |
|
48 \label{fig:keywords} |
|
49 \end{figure} |
|
50 |
|
51 \begin{figure}[htbp] |
|
52 \begin{center} |
|
53 \begin{tabular}{|lllll|} |
|
54 \hline |
|
55 \texttt{ALL} & |
|
56 \texttt{case} & |
|
57 \texttt{div} & |
|
58 \texttt{dvd} & |
|
59 \texttt{else} \\ |
|
60 \texttt{EX} & |
|
61 \texttt{if} & |
|
62 \texttt{in} & |
|
63 \texttt{INT} & |
|
64 \texttt{Int} \\ |
|
65 \texttt{LEAST} & |
|
66 \texttt{let} & |
|
67 \texttt{mod} & |
|
68 \texttt{O} & |
|
69 \texttt{o} \\ |
|
70 \texttt{of} & |
|
71 \texttt{op} & |
|
72 \texttt{PROP} & |
|
73 \texttt{SIGMA} & |
|
74 \texttt{then} \\ |
|
75 \texttt{Times} & |
|
76 \texttt{UN} & |
|
77 \texttt{Un} &&\\ |
|
78 \hline |
|
79 \end{tabular} |
|
80 \end{center} |
|
81 \caption{Reserved words in HOL} |
|
82 \label{fig:ReservedWords} |
|
83 \end{figure} |
|