Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more attribute tuning
authornipkow
Tue, 29 Oct 2024 10:26:06 +0100
changeset 81285 34f3ec8d4d24
parent 81284 f77c6448d4d7
child 81286 c2535056434f
more attribute tuning
src/HOL/List.thy file | annotate | diff | comparison | revisions 
--- 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)
isabelle