author | Christian Urban <urbanc@in.tum.de> |
Sat, 05 Nov 2011 18:44:28 +0000 | |
changeset 485 | f3536f0b47a9 |
parent 475 | 25371f74c768 |
child 517 | d8c376662bb4 |
permissions | -rw-r--r-- |
theory Appendix imports Base begin (*<*) setup{* open_file_with_prelude "Recipes_Code.thy" ["theory Recipes", "imports Main", "begin"] *} (*>*) text {* \appendix *} chapter {* Recipes *} text {* Possible topics: \begin{itemize} \item translations/print translations; @{ML "Proof_Context.print_syntax"} \item user space type systems (in the form that already exists) \item useful datastructures: discrimination nets, graphs, association lists \item Brief history of Isabelle \end{itemize} *} end