diff -r 8939b8fd8603 -r 069d525f8f1d CookBook/Appendix.thy --- a/CookBook/Appendix.thy Wed Mar 18 23:52:51 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ - -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 \ No newline at end of file