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}