# HG changeset patch
# User desharna
# Date 1671367985 -3600
# Node ID f572f5525e4bb49194a9a8bcc366c6e913dd187b
# Parent  186cf469b95dcaa8f0747ba9026bfdc257607838# Parent  0d7a9e4e1d61ee6ca5bbf765e7d5fdea5e4170cc
merged

diff -r 186cf469b95d -r f572f5525e4b NEWS
--- a/NEWS	Sat Dec 17 21:26:36 2022 +0100
+++ b/NEWS	Sun Dec 18 13:53:05 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]
diff -r 186cf469b95d -r f572f5525e4b src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Sat Dec 17 21:26:36 2022 +0100
+++ b/src/HOL/Equiv_Relations.thy	Sun Dec 18 13:53:05 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)
diff -r 186cf469b95d -r f572f5525e4b src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Sat Dec 17 21:26:36 2022 +0100
+++ b/src/HOL/Transitive_Closure.thy	Sun Dec 18 13:53:05 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)