diff -r 06e195515deb -r 87429bdecad5 src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Probability/Borel_Space.thy	Mon Jun 30 15:45:21 2014 +0200
@@ -141,6 +141,9 @@
 lemma cbox_borel[measurable]: "cbox a b \<in> sets borel"
   by (auto intro: borel_closed)
 
+lemma box_borel[measurable]: "box a b \<in> sets borel"
+  by (auto intro: borel_open)
+
 lemma borel_compact: "compact (A::'a::t2_space set) \<Longrightarrow> A \<in> sets borel"
   by (auto intro: borel_closed dest!: compact_imp_closed)
 
@@ -293,7 +296,6 @@
   fixes a b :: "'a\<Colon>ordered_euclidean_space"
   shows "{x. x <e a} \<in> sets borel"
     and "{x. a <e x} \<in> sets borel"
-    and "box a b \<in> sets borel"
     and "{..a} \<in> sets borel"
     and "{a..} \<in> sets borel"
     and "{a..b} \<in> sets borel"
@@ -605,6 +607,16 @@
        (auto intro!: sigma_sets_top)
 qed auto
 
+lemma borel_sigma_sets_Ioc: "borel = sigma UNIV (range (\<lambda>(a, b). {a <.. b::real}))"
+proof (rule borel_eq_sigmaI5[OF borel_eq_atMost])
+  fix i :: real
+  have "{..i} = (\<Union>j::nat. {-j <.. i})"
+    by (auto simp: minus_less_iff reals_Archimedean2)
+  also have "\<dots> \<in> sets (sigma UNIV (range (\<lambda>(i, j). {i<..j})))"
+    by (intro sets.countable_nat_UN) auto 
+  finally show "{..i} \<in> sets (sigma UNIV (range (\<lambda>(i, j). {i<..j})))" .
+qed simp
+
 lemma eucl_lessThan: "{x::real. x <e a} = lessThan a"
   by (simp add: eucl_less_def lessThan_def)
 
@@ -1307,6 +1319,73 @@
   shows "(\<lambda>x. suminf (\<lambda>i. f i x)) \<in> borel_measurable M"
   unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp
 
+(* Proof by Jeremy Avigad and Luke Serafin *)
+lemma isCont_borel:
+  fixes f :: "'b::metric_space \<Rightarrow> 'a::metric_space"
+  shows "{x. isCont f x} \<in> sets borel"
+proof -
+  let ?I = "\<lambda>j. inverse(real (Suc j))"
+
+  { fix x
+    have "isCont f x = (\<forall>i. \<exists>j. \<forall>y z. dist x y < ?I j \<and> dist x z < ?I j \<longrightarrow> dist (f y) (f z) \<le> ?I i)"
+      unfolding continuous_at_eps_delta
+    proof safe
+      fix i assume "\<forall>e>0. \<exists>d>0. \<forall>y. dist y x < d \<longrightarrow> dist (f y) (f x) < e"
+      moreover have "0 < ?I i / 2"
+        by simp
+      ultimately obtain d where d: "0 < d" "\<And>y. dist x y < d \<Longrightarrow> dist (f y) (f x) < ?I i / 2"
+        by (metis dist_commute)
+      then obtain j where j: "?I j < d"
+        by (metis reals_Archimedean)
+
+      show "\<exists>j. \<forall>y z. dist x y < ?I j \<and> dist x z < ?I j \<longrightarrow> dist (f y) (f z) \<le> ?I i"
+      proof (safe intro!: exI[where x=j])
+        fix y z assume *: "dist x y < ?I j" "dist x z < ?I j"
+        have "dist (f y) (f z) \<le> dist (f y) (f x) + dist (f z) (f x)"
+          by (rule dist_triangle2)
+        also have "\<dots> < ?I i / 2 + ?I i / 2"
+          by (intro add_strict_mono d less_trans[OF _ j] *)
+        also have "\<dots> \<le> ?I i"
+          by (simp add: field_simps real_of_nat_Suc)
+        finally show "dist (f y) (f z) \<le> ?I i"
+          by simp
+      qed
+    next
+      fix e::real assume "0 < e"
+      then obtain n where n: "?I n < e"
+        by (metis reals_Archimedean)
+      assume "\<forall>i. \<exists>j. \<forall>y z. dist x y < ?I j \<and> dist x z < ?I j \<longrightarrow> dist (f y) (f z) \<le> ?I i"
+      from this[THEN spec, of "Suc n"]
+      obtain j where j: "\<And>y z. dist x y < ?I j \<Longrightarrow> dist x z < ?I j \<Longrightarrow> dist (f y) (f z) \<le> ?I (Suc n)"
+        by auto
+      
+      show "\<exists>d>0. \<forall>y. dist y x < d \<longrightarrow> dist (f y) (f x) < e"
+      proof (safe intro!: exI[of _ "?I j"])
+        fix y assume "dist y x < ?I j"
+        then have "dist (f y) (f x) \<le> ?I (Suc n)"
+          by (intro j) (auto simp: dist_commute)
+        also have "?I (Suc n) < ?I n"
+          by simp
+        also note n
+        finally show "dist (f y) (f x) < e" .
+      qed simp
+    qed }
+  note * = this
+
+  have **: "\<And>e y. open {x. dist x y < e}"
+    using open_ball by (simp_all add: ball_def dist_commute)
+
+  have "{x\<in>space borel. isCont f x } \<in> sets borel"
+    unfolding *
+    apply (intro sets.sets_Collect_countable_All sets.sets_Collect_countable_Ex)
+    apply (simp add: Collect_all_eq)
+    apply (intro borel_closed closed_INT ballI closed_Collect_imp open_Collect_conj **)
+    apply auto
+    done
+  then show ?thesis
+    by simp
+qed
+
 no_notation
   eucl_less (infix "<e" 50)