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