--- 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'))"