# HG changeset patch
# User wenzelm
# Date 1194716166 -3600
# Node ID dca6916104890747cc57d81ce3479e4f41480b9e
# Parent  dcde128c84a2156fe8c19e4fe523d2548305413d
tuned document;

diff -r dcde128c84a2 -r dca691610489 src/HOL/Library/Binomial.thy
--- 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
diff -r dcde128c84a2 -r dca691610489 src/HOL/Library/Numeral_Type.thy
--- 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" *}