# HG changeset patch
# User desharna
# Date 1711391252 -3600
# Node ID 4f803ae647814ed360f50f6df83bba3cb1fa7cc7
# Parent  c2cca97a57978a6b9579cc2070984cbb62ba34db
changed number of consumed assumptions of wf_on_induct and wfp_on_induct

diff -r c2cca97a5797 -r 4f803ae64781 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Mon Mar 25 17:55:02 2024 +0100
+++ b/src/HOL/Wellfounded.thy	Mon Mar 25 19:27:32 2024 +0100
@@ -49,12 +49,12 @@
 
 subsection \<open>Induction Principles\<close>
 
-lemma wf_on_induct[consumes 2, case_names less, induct set: wf_on]:
+lemma wf_on_induct[consumes 1, case_names in_set less, induct set: wf_on]:
   assumes "wf_on A r" and "x \<in> A" and "\<And>x. x \<in> A \<Longrightarrow> (\<And>y. y \<in> A \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> P y) \<Longrightarrow> P x"
   shows "P x"
   using assms(2,3) by (auto intro: \<open>wf_on A r\<close>[unfolded wf_on_def, rule_format])
 
-lemma wfp_on_induct[consumes 2, case_names less, induct pred: wfp_on]:
+lemma wfp_on_induct[consumes 1, case_names in_set less, induct pred: wfp_on]:
   assumes "wfp_on A r" and "x \<in> A" and "\<And>x. x \<in> A \<Longrightarrow> (\<And>y. y \<in> A \<Longrightarrow> r y x \<Longrightarrow> P y) \<Longrightarrow> P x"
   shows "P x"
   using assms by (fact wf_on_induct[to_pred])
@@ -162,8 +162,12 @@
   shows "B = {}"
 proof -
   have "x \<notin> B" if "x \<in> A" for x
-    using wf that
+    using wf
   proof (induction x rule: wf_on_induct)
+    case in_set
+    show ?case
+      using that .
+  next
     case (less x)
     have "x \<notin> r `` B"
       using less.IH \<open>B \<subseteq> A\<close> by blast