src/HOL/List.thy
changeset 46439 2388be11cb50
parent 46424 b447318e5e1a
child 46440 d4994e2e7364
--- 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