--- a/src/HOL/Real.thy Sun Dec 23 15:40:28 2018 +0100
+++ b/src/HOL/Real.thy Sun Dec 23 20:51:23 2018 +0000
@@ -28,14 +28,6 @@
fixes n::nat shows "\<lbrakk>n \<le> m; n\<noteq>0\<rbrakk> \<Longrightarrow> 1 / of_nat m \<le> (1::'a::linordered_field) / of_nat n"
by (simp add: frac_le)
-lemma inj_add_left [simp]: "inj ((+) x)"
- for x :: "'a::cancel_semigroup_add"
- by (meson add_left_imp_eq injI)
-
-lemma inj_mult_left [simp]: "inj ((*) x) \<longleftrightarrow> x \<noteq> 0"
- for x :: "'a::idom"
- by (metis injI mult_cancel_left the_inv_f_f zero_neq_one)
-
lemma add_diff_add: "(a + c) - (b + d) = (a - b) + (c - d)"
for a b c d :: "'a::ab_group_add"
by simp