diff -r e5366291d6aa -r 8d5e5ec1cac3 src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Mon May 19 12:04:45 2014 +0200
+++ b/src/HOL/Probability/Information.thy	Mon May 19 13:44:13 2014 +0200
@@ -26,7 +26,7 @@
   "((A, B) = X) \<longleftrightarrow> (fst X = A \<and> snd X = B)" and
   "(X = (A, B)) \<longleftrightarrow> (fst X = A \<and> snd X = B)" by auto
 
-section "Information theory"
+subsection "Information theory"
 
 locale information_space = prob_space +
   fixes b :: real assumes b_gt_1: "1 < b"