tuned document;
authorwenzelm
Sat Nov 10 18:36:06 2007 +0100 (2007-11-10)
changeset 25378dca691610489
parent 25377 dcde128c84a2
child 25379 12bcf37252b1
tuned document;
src/HOL/Library/Binomial.thy
src/HOL/Library/Numeral_Type.thy
     1.1 --- a/src/HOL/Library/Binomial.thy	Sat Nov 10 18:36:06 2007 +0100
     1.2 +++ b/src/HOL/Library/Binomial.thy	Sat Nov 10 18:36:06 2007 +0100
     1.3 @@ -82,7 +82,7 @@
     1.4    done
     1.5  
     1.6  
     1.7 -subsubsection {* Theorems about @{text "choose"} *}
     1.8 +subsection {* Theorems about @{text "choose"} *}
     1.9  
    1.10  text {*
    1.11    \medskip Basic theorem about @{text "choose"}.  By Florian
     2.1 --- a/src/HOL/Library/Numeral_Type.thy	Sat Nov 10 18:36:06 2007 +0100
     2.2 +++ b/src/HOL/Library/Numeral_Type.thy	Sat Nov 10 18:36:06 2007 +0100
     2.3 @@ -85,6 +85,7 @@
     2.4    unfolding univ_set
     2.5    by (simp only: card_Pow finite numeral_2_eq_2)
     2.6  
     2.7 +
     2.8  subsection {* Numeral Types *}
     2.9  
    2.10  typedef (open) num0 = "UNIV :: nat set" ..
    2.11 @@ -140,9 +141,9 @@
    2.12    card_bit1
    2.13    card_num0
    2.14  
    2.15 +
    2.16  subsection {* Syntax *}
    2.17  
    2.18 -
    2.19  syntax
    2.20    "_NumeralType" :: "num_const => type"  ("_")
    2.21    "_NumeralType0" :: type ("0")
    2.22 @@ -204,7 +205,7 @@
    2.23  *}
    2.24  
    2.25  
    2.26 -subsection {* Classes with at values least 1 and 2  *}
    2.27 +subsection {* Classes with at least 1 and 2  *}
    2.28  
    2.29  text {* Class finite already captures "at least 1" *}
    2.30