src/HOL/Probability/ex/Dining_Cryptographers.thy

--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy	Mon May 19 12:04:45 2014 +0200
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy	Mon May 19 13:44:13 2014 +0200
@@ -8,7 +8,7 @@
 lemma Ex1_eq: "\<exists>!x. P x \<Longrightarrow> P x \<Longrightarrow> P y \<Longrightarrow> x = y"
   by auto
 
-section "Define the state space"
+subsection {* Define the state space *}
 
 text {*