--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ProgTutorial/Appendix.thy	Thu Mar 19 13:28:16 2009 +0100
@@ -0,0 +1,28 @@
+
+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