diff -r e8b9c0ebf5dd -r 83f1b16486ee TODO --- 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