# HG changeset patch
# User desharna
# Date 1710929464 -3600
# Node ID 5e85ea359563095a6a143bfb45d4b215ed760a8b
# Parent  b045d20c9c3c2bc2d590ef78c07f4239733e70fa
renamed lemma antisymp_on_reflcp to antisymp_on_reflclp

diff -r b045d20c9c3c -r 5e85ea359563 NEWS
--- a/NEWS	Wed Mar 20 09:57:14 2024 +0100
+++ b/NEWS	Wed Mar 20 11:11:04 2024 +0100
@@ -76,6 +76,8 @@
       transp_on_image
 
 * Theory "HOL.Transitive_Closure":
+  - Renamed lemma antisymp_on_reflcp to antisymp_on_reflclp.
+    Minor INCOMPATIBILITY.
   - Added lemmas.
       antisym_on_reflcl_if_asym_on
       antisymp_on_reflclp_if_asymp_on
diff -r b045d20c9c3c -r 5e85ea359563 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Wed Mar 20 09:57:14 2024 +0100
+++ b/src/HOL/Transitive_Closure.thy	Wed Mar 20 11:11:04 2024 +0100
@@ -79,7 +79,7 @@
 lemma antisym_on_reflcl[simp]: "antisym_on A (r\<^sup>=) \<longleftrightarrow> antisym_on A r"
   by (simp add: antisym_on_def)
 
-lemma antisymp_on_reflcp[simp]: "antisymp_on A R\<^sup>=\<^sup>= \<longleftrightarrow> antisymp_on A R"
+lemma antisymp_on_reflclp[simp]: "antisymp_on A R\<^sup>=\<^sup>= \<longleftrightarrow> antisymp_on A R"
   by (rule antisym_on_reflcl[to_pred])
 
 lemma trans_on_reflcl[simp]: "trans_on A r \<Longrightarrow> trans_on A (r\<^sup>=)"
@@ -91,7 +91,7 @@
 lemma antisymp_on_reflclp_if_asymp_on:
   assumes "asymp_on A R"
   shows "antisymp_on A R\<^sup>=\<^sup>="
-  unfolding antisymp_on_reflcp
+  unfolding antisymp_on_reflclp
   using antisymp_on_if_asymp_on[OF \<open>asymp_on A R\<close>] .
 
 lemma antisym_on_reflcl_if_asym_on: "asym_on A R \<Longrightarrow> antisym_on A (R\<^sup>=)"