src/HOL/Multivariate_Analysis/Integration.thy
changeset 36359 e5c785c166b2
parent 36334 068a01b4bc56
child 36362 06475a1547cb
     1.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Sun Apr 25 11:58:39 2010 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Sun Apr 25 16:23:40 2010 -0700
     1.3 @@ -3651,7 +3651,7 @@
     1.4  
     1.5  lemma indefinite_integral_continuous: fixes f::"real^1 \<Rightarrow> 'a::banach"
     1.6    assumes "f integrable_on {a..b}" shows  "continuous_on {a..b} (\<lambda>x. integral {a..x} f)"
     1.7 -proof(unfold continuous_on_def, safe)  fix x e assume as:"x\<in>{a..b}" "0<(e::real)"
     1.8 +proof(unfold continuous_on_iff, safe)  fix x e assume as:"x\<in>{a..b}" "0<(e::real)"
     1.9    let ?thesis = "\<exists>d>0. \<forall>x'\<in>{a..b}. dist x' x < d \<longrightarrow> dist (integral {a..x'} f) (integral {a..x} f) < e"
    1.10    { presume *:"a<b \<Longrightarrow> ?thesis"
    1.11      show ?thesis apply(cases,rule *,assumption)