Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/Refute_Examples.thy
changeset 25032 f7095d7cb9a3
parent 25031 4d1271cc42ea
child 28524 644b62cf678f 
--- 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
isabelle