1.1 --- a/src/HOL/Num.thy	Fri Mar 30 08:04:28 2012 +0200
     1.2 +++ b/src/HOL/Num.thy	Fri Mar 30 08:15:29 2012 +0200
     1.3 @@ -230,10 +230,10 @@
     1.4    by (simp add: num_eq_iff nat_of_num_sqr nat_of_num_mult)
     1.5  
     1.6  
     1.7 -subsection {* Numary numerals *}
     1.8 +subsection {* Binary numerals *}
     1.9  
    1.10  text {*
    1.11 -  We embed numary representations into a generic algebraic
    1.12 +  We embed binary representations into a generic algebraic
    1.13    structure using @{text numeral}.
    1.14  *}
    1.15  
    1.16 @@ -967,7 +967,7 @@
    1.17    "inverse Numeral1 = (Numeral1::'a::division_ring)"
    1.18    by simp
    1.19  
    1.20 -text{*Theorem lists for the cancellation simprocs. The use of a numary
    1.21 +text{*Theorem lists for the cancellation simprocs. The use of a binary
    1.22  numeral for 1 reduces the number of special cases.*}
    1.23  
    1.24  lemmas mult_1s =