src/HOL/Analysis/Complex_Analysis_Basics.thy
changeset 67979 53323937ee25
parent 67968 a5ad4c015d1c
child 68055 2cab37094fc4
     1.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Fri Apr 13 17:00:57 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sat Apr 14 09:23:00 2018 +0100
     1.3 @@ -1113,7 +1113,7 @@
     1.4      apply auto
     1.5      apply (rule_tac x="(1 - x) *\<^sub>R w + x *\<^sub>R z" in exI)
     1.6      apply (auto simp: closed_segment_def twz) []
     1.7 -    apply (intro derivative_eq_intros has_derivative_at_within, simp_all)
     1.8 +    apply (intro derivative_eq_intros has_derivative_at_withinI, simp_all)
     1.9      apply (simp add: fun_eq_iff real_vector.scale_right_diff_distrib)
    1.10      apply (force simp: twz closed_segment_def)
    1.11      done