diff -r 33f7201a0239 -r d51aab59bfbf TODO --- a/TODO Thu Apr 08 11:50:30 2010 +0200 +++ b/TODO Thu Apr 08 11:52:05 2010 +0200 @@ -39,8 +39,10 @@ equivalence creates more than one permutation. According to the paper, this is incorrect. - Example in TestMorePerm. + Example in Classical.thy. +- check whether weirdo example in TestMorePerm works + with shallow binders - nested recursion, like types "trm list" in a constructor