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