--- a/src/HOL/HOL.thy Tue Sep 24 21:41:01 2024 +0200
+++ b/src/HOL/HOL.thy Thu Sep 26 14:44:37 2024 +0100
@@ -633,6 +633,11 @@
shows R
using assms by (elim impCE)
+text \<open>The analogous introduction rule for conjunction, above, is even constructive\<close>
+lemma context_disjE:
+ assumes major: "P \<or> Q" and minor: "P \<Longrightarrow> R" "\<not>P \<Longrightarrow> Q \<Longrightarrow> R"
+ shows R
+ by (iprover intro: disjE [OF major] disjE [OF excluded_middle] assms)
text \<open>Classical \<open>\<longleftrightarrow>\<close> elimination.\<close>
lemma iffCE: