13
|
1 |
|
|
2 |
theory Appendix
|
|
3 |
imports Main
|
|
4 |
begin
|
|
5 |
|
182
|
6 |
|
13
|
7 |
text {* \appendix *}
|
|
8 |
|
129
|
9 |
|
13
|
10 |
chapter {* Recipes *}
|
|
11 |
|
131
|
12 |
text {*
|
184
|
13 |
Possible topics:
|
162
|
14 |
|
168
|
15 |
\begin{itemize}
|
|
16 |
\item translations/print translations;
|
162
|
17 |
@{ML "ProofContext.print_syntax"}
|
131
|
18 |
|
168
|
19 |
\item user space type systems (in the form that already exists)
|
164
|
20 |
|
184
|
21 |
\item unification and typing algorithms
|
|
22 |
(@{ML_file "Pure/pattern.ML"} implements HOPU)
|
164
|
23 |
|
168
|
24 |
\item useful datastructures: discrimination nets, association lists
|
|
25 |
\end{itemize}
|
131
|
26 |
*}
|
|
27 |
|
168
|
28 |
end |