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 \-Algebra *} +subsection {* Restricted Space Sigma Algebra *} definition "restrict_space M \ = measure_of \ ((op \ \) ` sets M) (\A. emeasure M (A \ \))"