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 redundant lemma
authornipkow
Tue, 11 Oct 2022 12:13:47 +0200
changeset 76260 5fd8ba24ca48
parent 76259 d1c26efb7a47
child 76261 26524d0b4395
removed redundant lemma
src/HOL/Fun.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Fun.thy	Tue Oct 11 10:45:42 2022 +0200
+++ b/src/HOL/Fun.thy	Tue Oct 11 12:13:47 2022 +0200
@@ -705,10 +705,6 @@
   "inj_on ((+) a) A"
   by (rule inj_onI) simp
 
-lemma inj_add_left:
-  \<open>inj ((+) a)\<close>
-  by simp
-
 lemma inj_on_add' [simp]:
   "inj_on (\<lambda>b. b + a) A"
   by (rule inj_onI) simp
isabelle