--- a/src/HOL/Probability/Borel_Space.thy Tue Nov 06 15:15:33 2012 +0100
+++ b/src/HOL/Probability/Borel_Space.thy Tue Nov 06 19:18:35 2012 +0100
@@ -74,7 +74,7 @@
using assms[of S] by simp
qed
-lemma borel_measurable_const[measurable (raw)]:
+lemma borel_measurable_const:
"(\<lambda>x. c) \<in> borel_measurable M"
by auto
@@ -168,7 +168,8 @@
shows borel_measurable_le[measurable]: "{w \<in> space M. f w \<le> g w} \<in> sets M"
and borel_measurable_eq[measurable]: "{w \<in> space M. f w = g w} \<in> sets M"
and borel_measurable_neq: "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
- unfolding eq_iff not_less[symmetric] by measurable+
+ unfolding eq_iff not_less[symmetric]
+ by measurable
subsection "Borel space equals sigma algebras over intervals"