diff -r 594356f16810 -r 82c20eaad94a src/HOL/List.thy --- a/src/HOL/List.thy Sun Jun 09 22:40:13 2024 +0200 +++ b/src/HOL/List.thy Mon Jun 10 08:25:55 2024 +0200 @@ -7383,7 +7383,7 @@ qed lemma wf_listrel1_iff[simp]: "wf(listrel1 r) = wf r" -by (auto simp: wf_acc_iff +by (auto simp: wf_iff_acc intro: lists_accD lists_accI[THEN Cons_in_lists_iff[THEN iffD1, THEN conjunct1]]) subsubsection \Lifting Relations to Lists: all elements\