diff -r b87b14e885af -r 43f5dfb7fa35 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/HOL.thy	Fri Jul 22 14:39:56 2022 +0200
@@ -745,13 +745,13 @@
 subsubsection \<open>Atomizing elimination rules\<close>
 
 lemma atomize_exL[atomize_elim]: "(\<And>x. P x \<Longrightarrow> Q) \<equiv> ((\<exists>x. P x) \<Longrightarrow> Q)"
-  by rule iprover+
+  by (rule equal_intr_rule) iprover+
 
 lemma atomize_conjL[atomize_elim]: "(A \<Longrightarrow> B \<Longrightarrow> C) \<equiv> (A \<and> B \<Longrightarrow> C)"
-  by rule iprover+
+  by (rule equal_intr_rule) iprover+
 
 lemma atomize_disjL[atomize_elim]: "((A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C) \<equiv> ((A \<or> B \<Longrightarrow> C) \<Longrightarrow> C)"
-  by rule iprover+
+  by (rule equal_intr_rule) iprover+
 
 lemma atomize_elimL[atomize_elim]: "(\<And>B. (A \<Longrightarrow> B) \<Longrightarrow> B) \<equiv> Trueprop A" ..
 
@@ -1923,7 +1923,7 @@
   by (rule ext equal_eq)+
 
 lemma equal_refl: "equal x x \<longleftrightarrow> True"
-  unfolding equal by rule+
+  unfolding equal by (rule iffI TrueI refl)+
 
 lemma eq_equal: "(=) \<equiv> equal"
   by (rule eq_reflection) (rule ext, rule ext, rule sym, rule equal_eq)