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