src/HOL/Integ/NatBin.thy
changeset 10574 8f98f0301d67
parent 9509 0f3ee1f89ca8
child 11464 ddea204de5bc
     1.1 --- a/src/HOL/Integ/NatBin.thy	Fri Dec 01 19:44:48 2000 +0100
     1.2 +++ b/src/HOL/Integ/NatBin.thy	Fri Dec 01 19:53:29 2000 +0100
     1.3 @@ -8,14 +8,16 @@
     1.4  This case is simply reduced to that for the non-negative integers
     1.5  *)
     1.6  
     1.7 -NatBin = IntPower +
     1.8 +theory NatBin = IntPower
     1.9 +files ("nat_bin.ML"):
    1.10  
    1.11 -instance
    1.12 -  nat :: number 
    1.13 +instance  nat :: number ..
    1.14  
    1.15  defs
    1.16 -  nat_number_of_def
    1.17 +  nat_number_of_def:
    1.18      "number_of v == nat (number_of v)"
    1.19       (*::bin=>nat        ::bin=>int*)
    1.20  
    1.21 +use "nat_bin.ML"	setup nat_bin_arith_setup
    1.22 +
    1.23  end