src/HOL/Probability/Lebesgue_Measure.thy
changeset 51478 270b21f3ae0a
parent 51000 c9adb50f74ad
child 53015 a1119cf551e8
     1.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Fri Mar 22 10:41:43 2013 +0100
     1.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Fri Mar 22 10:41:43 2013 +0100
     1.3 @@ -1049,7 +1049,7 @@
     1.4  
     1.5      let ?g = "\<lambda>x. if x = a then f a else if x = b then f b else if x \<in> {a <..< b} then f x else 0"
     1.6      from f have "continuous_on {a <..< b} f"
     1.7 -      by (subst continuous_on_eq_continuous_at) (auto simp add: continuous_isCont)
     1.8 +      by (subst continuous_on_eq_continuous_at) auto
     1.9      then have "?g \<in> borel_measurable borel"
    1.10        using borel_measurable_continuous_on_open[of "{a <..< b }" f "\<lambda>x. x" borel 0]
    1.11        by (auto intro!: measurable_If[where P="\<lambda>x. x = a"] measurable_If[where P="\<lambda>x. x = b"])