src/HOL/Library/Numeral_Type.thy
changeset 25378 dca691610489
parent 24630 351a308ab58d
child 25459 d1dce7d0731c
     1.1 --- a/src/HOL/Library/Numeral_Type.thy	Sat Nov 10 18:36:06 2007 +0100
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Sat Nov 10 18:36:06 2007 +0100
     1.3 @@ -85,6 +85,7 @@
     1.4    unfolding univ_set
     1.5    by (simp only: card_Pow finite numeral_2_eq_2)
     1.6  
     1.7 +
     1.8  subsection {* Numeral Types *}
     1.9  
    1.10  typedef (open) num0 = "UNIV :: nat set" ..
    1.11 @@ -140,9 +141,9 @@
    1.12    card_bit1
    1.13    card_num0
    1.14  
    1.15 +
    1.16  subsection {* Syntax *}
    1.17  
    1.18 -
    1.19  syntax
    1.20    "_NumeralType" :: "num_const => type"  ("_")
    1.21    "_NumeralType0" :: type ("0")
    1.22 @@ -204,7 +205,7 @@
    1.23  *}
    1.24  
    1.25  
    1.26 -subsection {* Classes with at values least 1 and 2  *}
    1.27 +subsection {* Classes with at least 1 and 2  *}
    1.28  
    1.29  text {* Class finite already captures "at least 1" *}
    1.30