13
|
1 |
|
|
2 |
theory Appendix
|
346
|
3 |
imports Base
|
13
|
4 |
begin
|
|
5 |
|
|
6 |
text {* \appendix *}
|
|
7 |
|
129
|
8 |
|
13
|
9 |
chapter {* Recipes *}
|
|
10 |
|
131
|
11 |
text {*
|
184
|
12 |
Possible topics:
|
162
|
13 |
|
168
|
14 |
\begin{itemize}
|
|
15 |
\item translations/print translations;
|
475
|
16 |
@{ML "Proof_Context.print_syntax"}
|
131
|
17 |
|
168
|
18 |
\item user space type systems (in the form that already exists)
|
164
|
19 |
|
407
|
20 |
\item useful datastructures: discrimination nets, graphs, association lists
|
356
|
21 |
|
|
22 |
\item Brief history of Isabelle
|
168
|
23 |
\end{itemize}
|
131
|
24 |
*}
|
|
25 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
26 |
end
|