diff -r 40f5c6b2e8aa -r 7f6178b655a8 src/HOL/Library/Rewrite.thy
--- a/src/HOL/Library/Rewrite.thy	Thu Oct 28 18:37:33 2021 +0200
+++ b/src/HOL/Library/Rewrite.thy	Thu Oct 28 20:01:59 2021 +0200
@@ -14,14 +14,6 @@
   fixes f :: "'a::{} \<Rightarrow> 'b::{}"
   shows "f \<equiv> \<lambda>x. f x" .
 
-lemma rewr_imp:
-  assumes "PROP A \<equiv> PROP B"
-  shows "(PROP A \<Longrightarrow> PROP C) \<equiv> (PROP B \<Longrightarrow> PROP C)"
-  apply (rule Pure.equal_intr_rule)
-  apply (drule equal_elim_rule2[OF assms]; assumption)
-  apply (drule equal_elim_rule1[OF assms]; assumption)
-  done
-
 lemma imp_cong_eq:
   "(PROP A \<Longrightarrow> (PROP B \<Longrightarrow> PROP C) \<equiv> (PROP B' \<Longrightarrow> PROP C')) \<equiv>
     ((PROP B \<Longrightarrow> PROP A \<Longrightarrow> PROP C) \<equiv> (PROP B' \<Longrightarrow> PROP A \<Longrightarrow> PROP C'))"