# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1270720325 -7200
# Node ID d51aab59bfbfb3f9fbd47f010cfb19d213692c48
# Parent  33f7201a02399dd9433fa085d897bafa49a08bf8
updated (comment about weirdo example)

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