# HG changeset patch
# User nipkow
# Date 1730193966 -3600
# Node ID 34f3ec8d4d24271836510e1133b8e816c54a5625
# Parent  f77c6448d4d71ad1767bad8fad0c627739dc0a9d
more attribute tuning

diff -r f77c6448d4d7 -r 34f3ec8d4d24 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Oct 29 07:41:52 2024 +0100
+++ b/src/HOL/List.thy	Tue Oct 29 10:26:06 2024 +0100
@@ -1239,7 +1239,7 @@
 lemma rev_eq_Cons_iff[iff]: "(rev xs = y#ys) = (xs = rev ys @ [y])"
 by (simp add: rev_swap)
 
-lemmas Cons_eq_rev_iff[iff] = rev_eq_Cons_iff[THEN eq_iff_swap]
+lemmas Cons_eq_rev_iff = rev_eq_Cons_iff[THEN eq_iff_swap]
 
 lemma inj_on_rev[iff]: "inj_on rev A"
 by(simp add:inj_on_def)