
diff -r 4d1271cc42ea -r f7095d7cb9a3 src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Mon Oct 15 01:36:22 2007 +0200
+++ b/src/HOL/ex/Refute_Examples.thy	Mon Oct 15 01:57:50 2007 +0200
@@ -1400,7 +1400,6 @@
   refute
 oops
 
-(* TODO: an efficient interpreter for @ is needed here
 lemma "xs @ [] = ys @ []"
   refute
 oops
@@ -1408,7 +1407,6 @@
 lemma "xs @ ys = ys @ xs"
   refute
 oops
-*)
 
 lemma "f (lfp f) = lfp f"
   refute




