# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1308530337 -32400
# Node ID 1628e47fa57c7dfa5c5a9cbcfdb3f0106774a6a2
# Parent  fac8b28f2a235a70e05c909139a4a37be1bda5a4
More minor TODOs

diff -r fac8b28f2a23 -r 1628e47fa57c TODO
--- 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: