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.
removed unused universal variable from lemma reflp_onI
authordesharna
Mon, 10 Oct 2022 19:07:54 +0200
changeset 76256 207b6fcfc47d
parent 76255 b3ff4f171eda
child 76257 61a5b5ad3a6e
child 76259 d1c26efb7a47
removed unused universal variable from lemma reflp_onI
src/HOL/Relation.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Relation.thy	Mon Oct 10 13:42:14 2022 +0200
+++ b/src/HOL/Relation.thy	Mon Oct 10 19:07:54 2022 +0200
@@ -173,7 +173,7 @@
   unfolding refl_on_def by (iprover intro!: ballI)
 
 lemma reflp_onI:
-  "(\<And>x y. x \<in> A \<Longrightarrow> R x x) \<Longrightarrow> reflp_on A R"
+  "(\<And>x. x \<in> A \<Longrightarrow> R x x) \<Longrightarrow> reflp_on A R"
   by (simp add: reflp_on_def)
 
 lemma reflpI[intro?]: "(\<And>x. R x x) \<Longrightarrow> reflp R"
isabelle