src/HOL/Analysis/Complex_Analysis_Basics.thy
changeset 66089 def95e0bc529
parent 65587 16a8991ab398
child 66252 b73f94b366b7
     1.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Thu Jun 15 11:11:36 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Thu Jun 15 17:22:23 2017 +0100
     1.3 @@ -919,7 +919,6 @@
     1.4    apply (auto simp:  bounded_linear_mult_right)
     1.5    done
     1.6  
     1.7 -(*Used only once, in Multivariate/cauchy.ml. *)
     1.8  lemma has_complex_derivative_inverse_strong:
     1.9    fixes f :: "complex \<Rightarrow> complex"
    1.10    shows "DERIV f x :> f' \<Longrightarrow>