--- a/src/HOL/Real.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Real.thy Wed Jan 10 15:25:09 2018 +0100
@@ -28,11 +28,11 @@
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 (op + x)"
+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 (op * x) \<longleftrightarrow> x \<noteq> 0"
+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)