Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added lemma reflp_on_reflclp[simp]
authordesharna
Wed, 09 Nov 2022 16:39:45 +0100
changeset 76496 855b5f0456d8
parent 76495 a718547c3493
child 76497 ebcfaddd3cb6
added lemma reflp_on_reflclp[simp]
NEWS file | annotate | diff | comparison | revisions
src/HOL/Transitive_Closure.thy file | annotate | diff | comparison | revisions 
--- a/NEWS	Wed Nov 09 16:45:12 2022 +0100
+++ b/NEWS	Wed Nov 09 16:39:45 2022 +0100
@@ -50,6 +50,8 @@
 * Theory "HOL.Transitive_Closure":
   - Strengthened lemma reflp_rtranclp and renamed to reflp_on_rtranclp.
     Minor INCOMPATIBILITY.
+  - Added lemmas.
+      reflp_on_reflclp[simp]
 
 * Theory "HOL.Wellfounded":
   - Added lemmas.
--- a/src/HOL/Transitive_Closure.thy	Wed Nov 09 16:45:12 2022 +0100
+++ b/src/HOL/Transitive_Closure.thy	Wed Nov 09 16:39:45 2022 +0100
@@ -70,6 +70,9 @@
 lemma refl_reflcl[simp]: "refl (r\<^sup>=)"
   by (simp add: refl_on_def)
 
+lemma reflp_on_reflclp[simp]: "reflp_on A R\<^sup>=\<^sup>="
+  by (simp add: reflp_on_def)
+
 lemma antisym_reflcl[simp]: "antisym (r\<^sup>=) = antisym r"
   by (simp add: antisym_def)
isabelle