--- a/TODO	Sun Jul 25 22:42:21 2010 +0200
+++ b/TODO	Mon Jul 26 09:19:28 2010 +0200
@@ -35,30 +35,6 @@
 - Parser adds syntax for raw datatype, but should
   add for lifted datatype.
 
-- the alpha equivalence for
-
-   Let as::assn t::trm   bind "bn as" in t
-
-  creates as premise
-
-    EX pi. as ~~bn as' /\ (bn as, t) ~~lst (bn as', t')
-
-  but I think it should be
-
-    as ~~bn as' /\ EX pi. (bn as, t) ~~lst (bn as', t')    
-
-  (both are equivalent, but the second seems to be closer to
-   the fv-function)
-
-- when there are more than one shallow binder, then alpha
-  equivalence creates more than one permutation. According
-  to the paper, this is incorrect.
-
-  Example in Classical.thy.
-
-- check whether weirdo example in TestMorePerm works
-  with shallow binders
-
 - nested recursion, like types "trm list" in a constructor
 
 - define permute_bn automatically and prove properties of it