author | Christian Urban <urbanc@in.tum.de> |
Tue, 31 Mar 2009 15:48:53 +0100 | |
changeset 215 | 8d1a344a621e |
parent 189 | 069d525f8f1d |
child 346 | 0fea8b7a14a1 |
permissions | -rw-r--r-- |
theory Appendix imports Main begin text {* \appendix *} chapter {* Recipes *} text {* Possible topics: \begin{itemize} \item translations/print translations; @{ML "ProofContext.print_syntax"} \item user space type systems (in the form that already exists) \item unification and typing algorithms (@{ML_file "Pure/pattern.ML"} implements HOPU) \item useful datastructures: discrimination nets, association lists \end{itemize} *} end