Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/List.thy
changeset 82771 40e4e955c846
parent 82736 1ca8d9705e34
child 82774 2865a6618cba 
--- a/src/HOL/List.thy	Wed Jun 25 16:35:25 2025 +0200
+++ b/src/HOL/List.thy	Thu Jun 26 17:30:16 2025 +0200
@@ -3417,7 +3417,7 @@
     "\<And>w x y z. f w x = f y z \<longleftrightarrow> w = y \<and> x = z" and
     "\<And>x y. f x y \<noteq> a" and
     "\<And>x y. f x y \<noteq> b"
-  shows "foldr f xs a = foldr f ys b \<longleftrightarrow> a = b \<and> xs = ys"
+  shows "foldr f xs a = foldr f ys b \<longleftrightarrow> xs = ys \<and> a = b"
 by (induction xs ys rule: list_induct2') (use assms(2,3,1) in auto)
isabelle