# 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