# HG changeset patch
# User hoelzl
# Date 1412683344 -7200
# Node ID 5b7f0b5da8848553550d156d7b1a30faf5058f03
# Parent  1f90ea1b40104bded42ad13562624e93196e82b9
fix document generation for HOL-Probability

diff -r 1f90ea1b4010 -r 5b7f0b5da884 src/HOL/Probability/Giry_Monad.thy
--- 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)"
diff -r 1f90ea1b4010 -r 5b7f0b5da884 src/HOL/Probability/Sigma_Algebra.thy
--- 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}"
diff -r 1f90ea1b4010 -r 5b7f0b5da884 src/HOL/Probability/document/root.tex
--- 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}