ProgTutorial/Appendix.thy
changeset 407 aee4abd02db1
parent 356 43df2d59fb98
child 475 25371f74c768
--- a/ProgTutorial/Appendix.thy	Wed Dec 02 02:34:09 2009 +0100
+++ b/ProgTutorial/Appendix.thy	Wed Dec 02 03:46:32 2009 +0100
@@ -25,10 +25,7 @@
   
   \item user space type systems (in the form that already exists)
 
-  \item unification and typing algorithms 
-  (@{ML_file "Pure/pattern.ML"} implements HOPU)
-
-  \item useful datastructures: discrimination nets, association lists
+  \item useful datastructures: discrimination nets, graphs, association lists
 
   \item Brief history of Isabelle
   \end{itemize}