src/HOL/Probability/Borel_Space.thy

 proof (rule measurable_measure_of, simp_all)
   fix S :: "'x set" assume "open S" thus "f -` S \<inter> space M \<in> sets M"
     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
 
 lemma borel_measurable_indicator:
   assumes A: "A \<in> sets M"

   assumes f[measurable]: "f \<in> borel_measurable M"
   assumes g[measurable]: "g \<in> borel_measurable M"
   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"
 
 lemma rational_boxes:
   fixes x :: "'a\<Colon>ordered_euclidean_space"