--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/TODO	Thu Mar 18 10:05:36 2010 +0100
@@ -0,0 +1,21 @@
+Smaller things:
+
+- case names for "weak" induction rules (names of the 
+constructors); see page 61/62 and 170 in Tutorial
+
+- <type>_perm rules should be added to the simplifier;
+  maybe <type>_perm whould be called permute_<type>.simps;
+  that would conform with the terminology in Nominal2
+
+- <type>_fv / <type>_bn / <type>_distinct should also be 
+  added to the simplifier
+
+
+Bigger things:
+
+- nested recursion, like types "trm list" in a constructor
+
+- strong induction rules
+
+
+What are the proofs that are still proved by sorry?
\ No newline at end of file