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" *}