--- 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