--- a/TODO	Mon Jun 20 09:36:16 2011 +0900
+++ b/TODO	Mon Jun 20 09:38:57 2011 +0900
@@ -29,6 +29,13 @@
 - maybe <t1_t2>.perm_simps should be called permute_<type>.simps;
   that would conform with the terminology in Nominal2
 
+- nominal_induct does not work without an induction rule
+
+- nominal_induct throws strange "THM" exceptions if not enough
+  variables are given
+
+- nominal_induct cannot avoid a term (for example function applied
+  to an argument).
 
 Other: