# HG changeset patch
# User nipkow
# Date 1665483227 -7200
# Node ID 5fd8ba24ca487bcf736847f62b66067a24906bd8
# Parent  d1c26efb7a47f35c19922b6d6ab7cb69a3c3c4d5
removed redundant lemma

diff -r d1c26efb7a47 -r 5fd8ba24ca48 src/HOL/Fun.thy
--- 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