diff -r c6f35921056e -r ab93d0190a5d src/HOL/Probability/Borel_Space.thy --- a/src/HOL/Probability/Borel_Space.thy Tue Jul 19 14:37:49 2011 +0200 +++ b/src/HOL/Probability/Borel_Space.thy Tue Jul 19 14:38:29 2011 +0200 @@ -1122,7 +1122,7 @@ show "(real -` B \ space borel :: ereal set) \ sets borel" proof cases assume "0 \ B" - then have *: "real -` B = real -` (B - {0}) \ {-\, \, 0}" + then have *: "real -` B = real -` (B - {0}) \ {-\, \, 0::ereal}" by (auto simp add: real_of_ereal_eq_0) then show "(real -` B :: ereal set) \ space borel \ sets borel" using open_real by auto @@ -1148,7 +1148,8 @@ qed auto lemma (in sigma_algebra) borel_measurable_ereal_iff_real: - "f \ borel_measurable M \ + fixes f :: "'a \ ereal" + shows "f \ borel_measurable M \ ((\x. real (f x)) \ borel_measurable M \ f -` {\} \ space M \ sets M \ f -` {-\} \ space M \ sets M)" proof safe assume *: "(\x. real (f x)) \ borel_measurable M" "f -` {\} \ space M \ sets M" "f -` {-\} \ space M \ sets M" @@ -1208,7 +1209,8 @@ qed auto lemma (in sigma_algebra) borel_measurable_eq_atMost_ereal: - "(f::'a \ ereal) \ borel_measurable M \ (\a. f -` {..a} \ space M \ sets M)" + fixes f :: "'a \ ereal" + shows "f \ borel_measurable M \ (\a. f -` {..a} \ space M \ sets M)" proof (intro iffI allI) assume pos[rule_format]: "\a. f -` {..a} \ space M \ sets M" show "f \ borel_measurable M" @@ -1226,7 +1228,7 @@ by (auto simp: not_le) then show "f -` {\} \ space M \ sets M" using pos by (auto simp del: UN_simps intro!: Diff) moreover - have "{-\} = {..-\}" by auto + have "{-\::ereal} = {..-\}" by auto then show "f -` {-\} \ space M \ sets M" using pos by auto moreover have "{x\space M. f x \ ereal a} \ sets M" using pos[of "ereal a"] by (simp add: vimage_def Int_def conj_commute)