diff -r bd94b0a71dd2 -r 630981482718 TODO
--- a/TODO	Wed Nov 24 19:51:33 2004 +0100
+++ b/TODO	Thu Nov 25 12:39:12 2004 +0100
@@ -13,4 +13,15 @@
   language specification (cf. http://validator.w3.org/) (Tjark, or anyone
   who is interested)
 
+- eliminate the last remaining old-style theories (Larry):  
+  Datatype_Universe.ML
+  Gfp.ML
+  HOL_lemmas.ML
+  Lfp.ML
+  NatArith.ML
+  Relation_Power.ML
+  Sum_Type.ML
+  Wellfounded_Recursion.ML
+  Wellfounded_Relations.ML
+
 - remove this file (Tobias)