--- a/src/HOL/Probability/Radon_Nikodym.thy Sun Jun 26 19:10:03 2011 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy Mon Jun 27 09:42:46 2011 +0200
@@ -314,10 +314,6 @@
qed
qed
-lemma (in finite_measure) real_measure:
- assumes A: "A \<in> sets M" shows "\<exists>r. 0 \<le> r \<and> \<mu> A = extreal r"
- using finite_measure[OF A] positive_measure[OF A] by (cases "\<mu> A") auto
-
lemma (in finite_measure) Radon_Nikodym_finite_measure:
assumes "finite_measure (M\<lparr> measure := \<nu>\<rparr>)" (is "finite_measure ?M'")
assumes "absolutely_continuous \<nu>"