Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Transitive_Closure.thy
changeset 79940 5e85ea359563
parent 79939 b045d20c9c3c 
--- 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>=)"
isabelle