theory Appendiximports Mainbegintext {* \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