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