diff -r 3e30ea95c7aa -r 009ca4807baa CookBook/Appendix.thy
--- a/CookBook/Appendix.thy	Wed Mar 11 17:38:17 2009 +0000
+++ b/CookBook/Appendix.thy	Wed Mar 11 22:34:49 2009 +0000
@@ -11,23 +11,16 @@
 text {*
   Possible further topics: 
 
-  translations/print translations
-
+  \begin{itemize}
+  \item translations/print translations; 
   @{ML "ProofContext.print_syntax"}
   
-  user space type systems (in the form that already exists)
-
-  unification and typing algorithms
+  \item user space type systems (in the form that already exists)
 
-  useful datastructures:
+  \item unification and typing algorithms
 
-  discrimination nets
-
-  association lists
+  \item useful datastructures: discrimination nets, association lists
+  \end{itemize}
 *}
 
-end
-  
-
-
-
+end
\ No newline at end of file