CookBook/Appendix.thy
changeset 170 90bee31628dc
parent 168 009ca4807baa
child 182 4d0e2edd476d
--- a/CookBook/Appendix.thy	Thu Feb 26 13:46:05 2009 +0100
+++ b/CookBook/Appendix.thy	Thu Mar 12 08:11:02 2009 +0100
@@ -5,21 +5,22 @@
 
 text {* \appendix *}
 
-text {*
-  Possible topics: translations/print translations
-*}
-
 
 chapter {* Recipes *}
 
 text {*
-  Possible topics: translations/print translations
+  Possible further topics: 
+
+  \begin{itemize}
+  \item translations/print translations; 
+  @{ML "ProofContext.print_syntax"}
   
-  User Space Type Systems (in the already existing form)
+  \item user space type systems (in the form that already exists)
+
+  \item unification and typing algorithms
+
+  \item useful datastructures: discrimination nets, association lists
+  \end{itemize}
 *}
 
-end
-  
-
-
-
+end
\ No newline at end of file