# HG changeset patch
# User desharna
# Date 1671183298 -3600
# Node ID 0d7a9e4e1d61ee6ca5bbf765e7d5fdea5e4170cc
# Parent  8fff4e4d81cb2e4cfb3af749fa209e177df93939
strengthened and renamed symp_symclp

diff -r 8fff4e4d81cb -r 0d7a9e4e1d61 NEWS
--- 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]
diff -r 8fff4e4d81cb -r 0d7a9e4e1d61 src/HOL/Equiv_Relations.thy
--- 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)
diff -r 8fff4e4d81cb -r 0d7a9e4e1d61 src/HOL/Transitive_Closure.thy
--- 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)