| author | nipkow |
| Thu, 26 Jun 2025 17:30:33 +0200 | |
| changeset 82772 | 59b937edcff8 |
| parent 82770 | 4a1320dac3f3 (current diff) |
| parent 82771 | 40e4e955c846 (diff) |
| child 82773 | 4ec8e654112f |
--- a/src/HOL/List.thy Thu Jun 26 17:16:14 2025 +0200 +++ b/src/HOL/List.thy Thu Jun 26 17:30:33 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)