src/HOL/NatBin.thy
changeset 25571 c9e39eafc7a0
parent 25481 aa16cd919dcc
child 25919 8b1c0d434824
     1.1 --- a/src/HOL/NatBin.thy	Fri Dec 07 15:07:56 2007 +0100
     1.2 +++ b/src/HOL/NatBin.thy	Fri Dec 07 15:07:59 2007 +0100
     1.3 @@ -14,8 +14,15 @@
     1.4    Arithmetic for naturals is reduced to that for the non-negative integers.
     1.5  *}
     1.6  
     1.7 -instance nat :: number
     1.8 -  nat_number_of_def [code inline]: "number_of v == nat (number_of (v\<Colon>int))" ..
     1.9 +instantiation nat :: number
    1.10 +begin
    1.11 +
    1.12 +definition
    1.13 +  nat_number_of_def [code inline]: "number_of v = nat (number_of (v\<Colon>int))"
    1.14 +
    1.15 +instance ..
    1.16 +
    1.17 +end
    1.18  
    1.19  abbreviation (xsymbols)
    1.20    square :: "'a::power => 'a"  ("(_\<twosuperior>)" [1000] 999) where