diff -r 83f36a1c62f2 -r 3fb9f820a294 CookBook/Appendix.thy
--- a/CookBook/Appendix.thy	Fri Mar 06 16:12:16 2009 +0000
+++ b/CookBook/Appendix.thy	Fri Mar 06 21:52:17 2009 +0000
@@ -5,17 +5,19 @@
 
 text {* \appendix *}
 
-text {*
-  Possible topics: translations/print translations
-*}
-
 
 chapter {* Recipes *}
 
 text {*
-  Possible topics: translations/print translations
+  Possible further topics: 
+
+  translations/print translations
+
+  @{ML "ProofContext.print_syntax"}
   
-  User Space Type Systems (in the already existing form)
+  user space type systems (in the form that already exists)
+
+  unification and typing algorithms
 *}
 
 end