diff -r 26ee9656872a -r 80369da39838 src/HOL/Library/Binomial.thy
--- a/src/HOL/Library/Binomial.thy	Fri Feb 13 14:41:54 2009 -0800
+++ b/src/HOL/Library/Binomial.thy	Fri Feb 13 14:45:10 2009 -0800
@@ -182,7 +182,7 @@
   finally show ?case by simp
 qed
 
-section{* Pochhammer's symbol : generalized raising factorial*}
+subsection{* Pochhammer's symbol : generalized raising factorial*}
 
 definition "pochhammer (a::'a::comm_semiring_1) n = (if n = 0 then 1 else setprod (\<lambda>n. a + of_nat n) {0 .. n - 1})"
 
@@ -285,7 +285,7 @@
     pochhammer_of_nat_eq_0_lemma'[of k n, where ?'a = 'a]
   by (auto simp add: not_le[symmetric])
 
-section{* Generalized binomial coefficients *}
+subsection{* Generalized binomial coefficients *}
 
 definition gbinomial :: "'a::{field, recpower,ring_char_0} \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
   where "a gchoose n = (if n = 0 then 1 else (setprod (\<lambda>i. a - of_nat i) {0 .. n - 1}) / of_nat (fact n))"