# HG changeset patch
# User blanchet
# Date 1328658906 -3600
# Node ID 2388be11cb50c90694e9e0c99f81634b0520e5b6
# Parent  93344b60cb301b2d429e6fb934404d74cde5304d
removed fact that confuses SPASS -- better rely on "rev_rev_ident", which is stronger and more ATP friendly

diff -r 93344b60cb30 -r 2388be11cb50 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Feb 08 00:05:22 2012 +0100
+++ b/src/HOL/List.thy	Wed Feb 08 00:55:06 2012 +0100
@@ -934,7 +934,7 @@
 lemma singleton_rev_conv [simp]: "([x] = rev xs) = (xs = [x])"
 by (cases xs) auto
 
-lemma rev_is_rev_conv [iff]: "(rev xs = rev ys) = (xs = ys)"
+lemma rev_is_rev_conv [iff, no_atp]: "(rev xs = rev ys) = (xs = ys)"
 apply (induct xs arbitrary: ys, force)
 apply (case_tac ys, simp, force)
 done