--- a/NEWS Fri Dec 16 10:30:15 2022 +0100
+++ b/NEWS Fri Dec 16 10:34:58 2022 +0100
@@ -94,6 +94,7 @@
- Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
antisym_reflcl[simp] ~> antisym_on_reflcl[simp]
reflp_rtranclp[simp] ~> reflp_on_rtranclp[simp]
+ symp_symclp[simp] ~> symp_on_symclp[simp]
- Added lemmas.
antisymp_on_reflcp[simp]
reflclp_ident_if_reflp[simp]
--- a/src/HOL/Equiv_Relations.thy Fri Dec 16 10:30:15 2022 +0100
+++ b/src/HOL/Equiv_Relations.thy Fri Dec 16 10:34:58 2022 +0100
@@ -486,7 +486,7 @@
lemma equivp_rtranclp: "symp r \<Longrightarrow> equivp r\<^sup>*\<^sup>*"
by(intro equivpI reflpI sympI transpI)(auto dest: sympD[OF symp_rtranclp])
-lemmas equivp_rtranclp_symclp [simp] = equivp_rtranclp[OF symp_symclp]
+lemmas equivp_rtranclp_symclp [simp] = equivp_rtranclp[OF symp_on_symclp]
lemma equivp_vimage2p: "equivp R \<Longrightarrow> equivp (vimage2p f f R)"
by(auto simp add: equivp_def vimage2p_def dest: fun_cong)
--- a/src/HOL/Transitive_Closure.thy Fri Dec 16 10:30:15 2022 +0100
+++ b/src/HOL/Transitive_Closure.thy Fri Dec 16 10:34:58 2022 +0100
@@ -759,8 +759,8 @@
lemma symclp_conversep [simp]: "symclp r\<inverse>\<inverse> = symclp r"
by(simp add: symclp_pointfree sup.commute)
-lemma symp_symclp [simp]: "symp (symclp r)"
- by(auto simp add: symp_def elim: symclpE intro: symclpI)
+lemma symp_on_symclp [simp]: "symp_on A (symclp R)"
+ by(auto simp add: symp_on_def elim: symclpE intro: symclpI)
lemma symp_symclp_eq: "symp r \<Longrightarrow> symclp r = r"
by(simp add: symclp_pointfree symp_conv_conversep_eq)