TODO

--- a/TODO	Wed Dec 08 07:50:27 2004 +0100
+++ b/TODO	Wed Dec 08 10:28:05 2004 +0100
@@ -15,11 +15,11 @@
 
 - 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
+  
+- update or remove ex/MT (Larry? Tobias?)  
 
 - remove this file (Tobias)