tuned attributes
authornipkow
Tue, 29 Oct 2024 07:41:52 +0100
changeset 81284 f77c6448d4d7
parent 81283 31a83265fa03
child 81285 34f3ec8d4d24
tuned attributes
src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Oct 28 18:48:28 2024 +0100
+++ b/src/HOL/List.thy	Tue Oct 29 07:41:52 2024 +0100
@@ -1233,13 +1233,13 @@
 lemma rev_eq_append_conv: "rev xs = ys @ zs \<longleftrightarrow> xs = rev zs @ rev ys"
 by (metis rev_append rev_rev_ident)
 
-lemma append_eq_rev_conv: "xs @ ys = rev zs \<longleftrightarrow> rev ys @ rev xs = zs"
-using rev_eq_append_conv[of zs xs ys] by auto
+lemma append_eq_rev_conv: "ys @ zs = rev xs \<longleftrightarrow> rev zs @ rev ys = xs"
+using rev_eq_append_conv[THEN eq_iff_swap] by metis
 
 lemma rev_eq_Cons_iff[iff]: "(rev xs = y#ys) = (xs = rev ys @ [y])"
 by (simp add: rev_swap)
 
-lemmas Cons_eq_rev_iff = rev_eq_Cons_iff[THEN eq_iff_swap]
+lemmas Cons_eq_rev_iff[iff] = rev_eq_Cons_iff[THEN eq_iff_swap]
 
 lemma inj_on_rev[iff]: "inj_on rev A"
 by(simp add:inj_on_def)