src/HOL/Deriv.thy

--- a/src/HOL/Deriv.thy	Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Deriv.thy	Wed Jan 10 15:25:09 2018 +0100
@@ -31,7 +31,7 @@
 
 definition has_field_derivative :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a filter \<Rightarrow> bool"
     (infix "(has'_field'_derivative)" 50)
-  where "(f has_field_derivative D) F \<longleftrightarrow> (f has_derivative op * D) F"
+  where "(f has_field_derivative D) F \<longleftrightarrow> (f has_derivative ( * ) D) F"
 
 lemma DERIV_cong: "(f has_field_derivative X) F \<Longrightarrow> X = Y \<Longrightarrow> (f has_field_derivative Y) F"
   by simp
@@ -150,7 +150,7 @@
 
 lemma field_has_derivative_at:
   fixes x :: "'a::real_normed_field"
-  shows "(f has_derivative op * D) (at x) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
+  shows "(f has_derivative ( * ) D) (at x) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
   apply (unfold has_derivative_at)
   apply (simp add: bounded_linear_mult_right)
   apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
@@ -588,7 +588,7 @@
   by (rule has_derivative_eq_rhs[of f D]) (simp_all add: fun_eq_iff mult.commute)
 
 lemma has_field_derivative_imp_has_derivative:
-  "(f has_field_derivative D) F \<Longrightarrow> (f has_derivative op * D) F"
+  "(f has_field_derivative D) F \<Longrightarrow> (f has_derivative ( * ) D) F"
   by (simp add: has_field_derivative_def)
 
 lemma DERIV_subset:
@@ -615,7 +615,7 @@
   assume "f differentiable at x within s"
   then obtain f' where *: "(f has_derivative f') (at x within s)"
     unfolding differentiable_def by auto
-  then obtain c where "f' = (op * c)"
+  then obtain c where "f' = (( * ) c)"
     by (metis real_bounded_linear has_derivative_bounded_linear mult.commute fun_eq_iff)
   with * show "\<exists>D. (f has_real_derivative D) (at x within s)"
     unfolding has_field_derivative_def by auto
@@ -647,7 +647,7 @@
 lemma DERIV_def: "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
   unfolding field_has_derivative_at has_field_derivative_def has_field_derivative_iff ..
 
-lemma mult_commute_abs: "(\<lambda>x. x * c) = op * c"
+lemma mult_commute_abs: "(\<lambda>x. x * c) = ( * ) c"
   for c :: "'a::ab_semigroup_mult"
   by (simp add: fun_eq_iff mult.commute)
 
@@ -830,7 +830,7 @@
     ((\<lambda>x. f x * c) has_field_derivative D * c) (at x within s)"
   using DERIV_cmult by (auto simp add: ac_simps)
 
-lemma DERIV_cmult_Id [simp]: "(op * c has_field_derivative c) (at x within s)"
+lemma DERIV_cmult_Id [simp]: "(( * ) c has_field_derivative c) (at x within s)"
   using DERIV_ident [THEN DERIV_cmult, where c = c and x = x] by simp
 
 lemma DERIV_cdivide:
@@ -853,7 +853,7 @@
   shows "((\<lambda>x. inverse (f x)) has_field_derivative - (inverse (f x) * D * inverse (f x)))
     (at x within s)"
 proof -
-  have "(f has_derivative (\<lambda>x. x * D)) = (f has_derivative op * D)"
+  have "(f has_derivative (\<lambda>x. x * D)) = (f has_derivative ( * ) D)"
     by (rule arg_cong [of "\<lambda>x. x * D"]) (simp add: fun_eq_iff)
   with assms have "(f has_derivative (\<lambda>x. x * D)) (at x within s)"
     by (auto dest!: has_field_derivative_imp_has_derivative)
@@ -906,7 +906,7 @@
 
 lemma DERIV_chain': "(f has_field_derivative D) (at x within s) \<Longrightarrow> DERIV g (f x) :> E \<Longrightarrow>
   ((\<lambda>x. g (f x)) has_field_derivative E * D) (at x within s)"
-  using has_derivative_compose[of f "op * D" x s g "op * E"]
+  using has_derivative_compose[of f "( * ) D" x s g "( * ) E"]
   by (simp only: has_field_derivative_def mult_commute_abs ac_simps)
 
 corollary DERIV_chain2: "DERIV f (g x) :> Da \<Longrightarrow> (g has_field_derivative Db) (at x within s) \<Longrightarrow>
@@ -924,7 +924,7 @@
   "(f has_field_derivative Da) (at (g x) within (g ` s)) \<Longrightarrow>
     (g has_field_derivative Db) (at x within s) \<Longrightarrow>
     (f \<circ> g has_field_derivative Da * Db) (at x within s)"
-  using has_derivative_in_compose [of g "op * Db" x s f "op * Da "]
+  using has_derivative_in_compose [of g "( * ) Db" x s f "( * ) Da "]
   by (simp add: has_field_derivative_def o_def mult_commute_abs ac_simps)
 
 (*These two are from HOL Light: HAS_COMPLEX_DERIVATIVE_CHAIN*)