removed fact that confuses SPASS -- better rely on "rev_rev_ident", which is stronger and more ATP friendly
authorblanchet
Wed Feb 08 00:55:06 2012 +0100 (2012-02-08)
changeset 464392388be11cb50
parent 46438 93344b60cb30
child 46440 d4994e2e7364
removed fact that confuses SPASS -- better rely on "rev_rev_ident", which is stronger and more ATP friendly
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Wed Feb 08 00:05:22 2012 +0100
     1.2 +++ b/src/HOL/List.thy	Wed Feb 08 00:55:06 2012 +0100
     1.3 @@ -934,7 +934,7 @@
     1.4  lemma singleton_rev_conv [simp]: "([x] = rev xs) = (xs = [x])"
     1.5  by (cases xs) auto
     1.6  
     1.7 -lemma rev_is_rev_conv [iff]: "(rev xs = rev ys) = (xs = ys)"
     1.8 +lemma rev_is_rev_conv [iff, no_atp]: "(rev xs = rev ys) = (xs = ys)"
     1.9  apply (induct xs arbitrary: ys, force)
    1.10  apply (case_tac ys, simp, force)
    1.11  done