diff -r 2319cff107f0 -r 3f617d7a2691 CookBook/Appendix.thy --- a/CookBook/Appendix.thy Sun Mar 08 20:53:00 2009 +0000 +++ b/CookBook/Appendix.thy Tue Mar 10 13:20:46 2009 +0000 @@ -18,6 +18,12 @@ user space type systems (in the form that already exists) unification and typing algorithms + + useful datastructures: + + discrimination nets + + association lists *} end