--- a/src/HOL/Probability/Giry_Monad.thy Tue Oct 07 10:48:29 2014 +0200
+++ b/src/HOL/Probability/Giry_Monad.thy Tue Oct 07 14:02:24 2014 +0200
@@ -817,7 +817,7 @@
finally show ?thesis ..
qed
-section {* Measures are \omega-chain complete partial orders *}
+section {* Measures form a $\omega$-chain complete partial order *}
definition SUP_measure :: "(nat \<Rightarrow> 'a measure) \<Rightarrow> 'a measure" where
"SUP_measure M = measure_of (\<Union>i. space (M i)) (\<Union>i. sets (M i)) (\<lambda>A. SUP i. emeasure (M i) A)"
--- 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}"
--- a/src/HOL/Probability/document/root.tex Tue Oct 07 10:48:29 2014 +0200
+++ b/src/HOL/Probability/document/root.tex Tue Oct 07 14:02:24 2014 +0200
@@ -6,6 +6,7 @@
\usepackage[only,bigsqcap]{stmaryrd}
\usepackage[utf8]{inputenc}
\usepackage{pdfsetup}
+\usepackage[english]{babel}
\urlstyle{rm}
\isabellestyle{it}