src/HOL/Probability/Borel_Space.thy
changeset 44282 f0de18b62d63
parent 43923 ab93d0190a5d
child 44537 c10485a6a7af
     1.1 --- a/src/HOL/Probability/Borel_Space.thy	Thu Aug 18 17:42:35 2011 +0200
     1.2 +++ b/src/HOL/Probability/Borel_Space.thy	Thu Aug 18 13:36:58 2011 -0700
     1.3 @@ -816,7 +816,7 @@
     1.4    proof cases
     1.5      assume "b \<noteq> 0"
     1.6      with `open S` have "((\<lambda>x. (- a + x) /\<^sub>R b) ` S) \<in> open" (is "?S \<in> open")
     1.7 -      by (auto intro!: open_affinity simp: scaleR.add_right mem_def)
     1.8 +      by (auto intro!: open_affinity simp: scaleR_add_right mem_def)
     1.9      hence "?S \<in> sets borel"
    1.10        unfolding borel_def by (auto simp: sigma_def intro!: sigma_sets.Basic)
    1.11      moreover