# HG changeset patch
# User hoelzl
# Date 1384331820 -3600
# Node ID 1e6412c82837207d0f154fa3237d7010285d931e
# Parent  0c50894fc0d986a3534da9c23417db083f40bd9f
fix document generation for HOL-Probability

diff -r 0c50894fc0d9 -r 1e6412c82837 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Tue Nov 12 20:08:29 2013 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Wed Nov 13 09:37:00 2013 +0100
@@ -1756,7 +1756,7 @@
   qed auto
 qed
 
-subsection {* Restricted Space \<sigma>-Algebra *}
+subsection {* Restricted Space Sigma Algebra *}
 
 definition "restrict_space M \<Omega> = measure_of \<Omega> ((op \<inter> \<Omega>) ` sets M) (\<lambda>A. emeasure M (A \<inter> \<Omega>))"