--- a/CookBook/Appendix.thy Tue Mar 17 17:32:12 2009 +0100
+++ b/CookBook/Appendix.thy Wed Mar 18 03:03:51 2009 +0100
@@ -10,7 +10,7 @@
chapter {* Recipes *}
text {*
- Possible further topics:
+ Possible topics:
\begin{itemize}
\item translations/print translations;
@@ -18,7 +18,8 @@
\item user space type systems (in the form that already exists)
- \item unification and typing algorithms
+ \item unification and typing algorithms
+ (@{ML_file "Pure/pattern.ML"} implements HOPU)
\item useful datastructures: discrimination nets, association lists
\end{itemize}