src/HOL/Probability/Probability_Measure.thy
changeset 45934 9321cd2572fe
parent 45777 c36637603821
child 46731 5302e932d1e5
     1.1 --- a/src/HOL/Probability/Probability_Measure.thy	Mon Dec 19 14:41:08 2011 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Tue Dec 20 11:40:56 2011 +0100
     1.3 @@ -1028,7 +1028,6 @@
     1.4      proof
     1.5        show "positive ?P (measure ?P)"
     1.6        proof (simp add: positive_def, safe)
     1.7 -        show "0 / \<mu> A = 0" using `\<mu> A \<noteq> 0` by (cases "\<mu> A") (auto simp: zero_ereal_def)
     1.8          fix B assume "B \<in> events"
     1.9          with real_measure[of "A \<inter> B"] real_measure[OF `A \<in> events`] `A \<in> sets M`
    1.10          show "0 \<le> \<mu> (A \<inter> B) / \<mu> A" by (auto simp: Int)