# 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>=) \ antisym_on A r" by (simp add: antisym_on_def) -lemma antisymp_on_reflcp[simp]: "antisymp_on A R\<^sup>=\<^sup>= \ antisymp_on A R" +lemma antisymp_on_reflclp[simp]: "antisymp_on A R\<^sup>=\<^sup>= \ antisymp_on A R" by (rule antisym_on_reflcl[to_pred]) lemma trans_on_reflcl[simp]: "trans_on A r \ 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 \asymp_on A R\] . lemma antisym_on_reflcl_if_asym_on: "asym_on A R \ antisym_on A (R\<^sup>=)"