src/HOL/Probability/Borel_Space.thy
changeset 56994 8d5e5ec1cac3
parent 56993 e5366291d6aa
child 57036 22568fb89165
--- a/src/HOL/Probability/Borel_Space.thy	Mon May 19 12:04:45 2014 +0200
+++ b/src/HOL/Probability/Borel_Space.thy	Mon May 19 13:44:13 2014 +0200
@@ -11,7 +11,7 @@
   "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
 begin
 
-section "Generic Borel spaces"
+subsection {* Generic Borel spaces *}
 
 definition borel :: "'a::topological_space measure" where
   "borel = sigma UNIV {S. open S}"
@@ -213,7 +213,7 @@
     unfolding eq by (rule borel_measurable_continuous_on[OF H]) auto
 qed
 
-section "Borel spaces on euclidean spaces"
+subsection {* Borel spaces on euclidean spaces *}
 
 lemma borel_measurable_inner[measurable (raw)]:
   fixes f g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_inner}"
@@ -1140,7 +1140,7 @@
   shows "(\<lambda>x. (\<Sum>i. f i x)) \<in> borel_measurable M"
   unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp
 
-section "LIMSEQ is borel measurable"
+subsection {* LIMSEQ is borel measurable *}
 
 lemma borel_measurable_LIMSEQ:
   fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> real"