equal
deleted
inserted
replaced
1 |
1 |
2 theory Appendix |
2 theory Appendix |
3 imports Base |
3 imports Base |
4 begin |
4 begin |
5 |
5 |
6 text {* \appendix *} |
6 text \<open>\appendix\<close> |
7 |
7 |
8 |
8 |
9 chapter {* Recipes *} |
9 chapter \<open>Recipes\<close> |
10 |
10 |
11 text {* |
11 text \<open> |
12 Possible topics: |
12 Possible topics: |
13 |
13 |
14 \begin{itemize} |
14 \begin{itemize} |
15 \item translations/print translations; |
15 \item translations/print translations; |
16 @{ML "Proof_Context.print_syntax"} |
16 @{ML "Proof_Context.print_syntax"} |
19 |
19 |
20 \item useful datastructures: discrimination nets, graphs, association lists |
20 \item useful datastructures: discrimination nets, graphs, association lists |
21 |
21 |
22 \item Brief history of Isabelle |
22 \item Brief history of Isabelle |
23 \end{itemize} |
23 \end{itemize} |
24 *} |
24 \<close> |
25 |
25 |
26 end |
26 end |