changeset 25378 | dca691610489 |
parent 25162 | ad4d5365d9d8 |
child 25594 | 43c718438f9f |
--- a/src/HOL/Library/Binomial.thy Sat Nov 10 18:36:06 2007 +0100 +++ b/src/HOL/Library/Binomial.thy Sat Nov 10 18:36:06 2007 +0100 @@ -82,7 +82,7 @@ done -subsubsection {* Theorems about @{text "choose"} *} +subsection {* Theorems about @{text "choose"} *} text {* \medskip Basic theorem about @{text "choose"}. By Florian