--- a/TODO	Thu Mar 18 15:13:20 2010 +0100
+++ b/TODO	Thu Mar 18 15:32:49 2010 +0100
@@ -1,8 +1,5 @@
 Smaller things:
 
-- case names for "weak" induction rules (names of the 
-constructors); see page 61/62 and 170 in Tutorial
-
 - maybe <type>_perm whould be called permute_<type>.simps;
   that would conform with the terminology in Nominal2