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