--- a/TODO	Sun Aug 29 01:45:07 2010 +0800
+++ b/TODO	Sun Aug 29 12:14:40 2010 +0800
@@ -1,16 +1,6 @@
-Automatically created functions:
-
-  ty1_tyn.bn[simp]        lifted equations for bn funs
-  ty1_tyn.fv[simp]        lifted equations for fv funs
-  ty1_tyn.perm[simp]      lifted permutation equations
-  ty1_tyn.distinct[simp]  lifted distincts
-  ty1_tyn.eq_iff
-  ty1_tyn.induct
-  ty1_tyn.inducts
-  instance ty1 and tyn :: fs
-  ty1_tyn.supp            empty when for too many bindings
 
 Parser should check that:
+
 - types of bindings match types of binding functions
 - fsets are not bound in lst bindings
 - bound arguments are not datatypes
@@ -18,22 +8,11 @@
 
 Smaller things:
 
-- lam.perm should be called permute_lam.simps (that is 
-  the convention from Nominal2)
-
 - maybe <type>_perm whould be called permute_<type>.simps;
   that would conform with the terminology in Nominal2
 
-- we also need to lift the size function for nominal
-  datatypes
 
-- Abs.thy contains lemmas for equivariance of the alphas;
-  they are not yet used anywhere
-
-Bigger things:
-
-- Parser adds syntax for raw datatype, but should
-  add for lifted datatype.
+Other:
 
 - nested recursion, like types "trm list" in a constructor
 
@@ -43,21 +22,6 @@
 
 - strong induction rules
 
-- check support equations for more bindings per constructor
-
-- For binding functions that call other binding functions
-  the following are proved with cheat_tac: constr_rsp
-
 - store information about defined nominal datatypes, so that
   it can be used to define new types that depend on these
 
-- make parser aware of recursive and of different versions of abs
-
-Less important:
-
-- fv_rsp uses 'blast' to show goals of the type:
-  a u b = c u d   ==>  a u x u b = c u x u d
-
-When cleaning:
-
-- remove all 'PolyML.makestring'.