--- a/src/HOL/Probability/Sigma_Algebra.thy Tue Oct 07 10:48:29 2014 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy Tue Oct 07 14:02:24 2014 +0200
@@ -2222,7 +2222,7 @@
using emeasure_extend_measure[OF M _ _ ms(2,3), of "(i,j)"] eq ms(1) `I i j`
by (auto simp: subset_eq)
-subsubsection {* Supremum of a set of \sigma-algebras *}
+subsubsection {* Supremum of a set of $\sigma$-algebras *}
definition "Sup_sigma M = sigma (\<Union>x\<in>M. space x) (\<Union>x\<in>M. sets x)"
@@ -2274,7 +2274,7 @@
using measurable_space[OF f] M by auto
qed (auto intro: measurable_sets f dest: sets.sets_into_space)
-subsection {* The smallest \sigma-algebra regarding a function *}
+subsection {* The smallest $\sigma$-algebra regarding a function *}
definition
"vimage_algebra X f M = sigma X {f -` A \<inter> X | A. A \<in> sets M}"