--- 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
--- a/src/HOL/Library/Numeral_Type.thy Sat Nov 10 18:36:06 2007 +0100
+++ b/src/HOL/Library/Numeral_Type.thy Sat Nov 10 18:36:06 2007 +0100
@@ -85,6 +85,7 @@
unfolding univ_set
by (simp only: card_Pow finite numeral_2_eq_2)
+
subsection {* Numeral Types *}
typedef (open) num0 = "UNIV :: nat set" ..
@@ -140,9 +141,9 @@
card_bit1
card_num0
+
subsection {* Syntax *}
-
syntax
"_NumeralType" :: "num_const => type" ("_")
"_NumeralType0" :: type ("0")
@@ -204,7 +205,7 @@
*}
-subsection {* Classes with at values least 1 and 2 *}
+subsection {* Classes with at least 1 and 2 *}
text {* Class finite already captures "at least 1" *}