src/HOL/Nat.thy
changeset 35121 36c0a6dd8c6f
parent 35064 1bdef0c013d3
child 35216 7641e8d831d2
     1.1 --- a/src/HOL/Nat.thy	Fri Feb 12 09:49:28 2010 +0100
     1.2 +++ b/src/HOL/Nat.thy	Fri Feb 12 14:28:01 2010 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  header {* Natural numbers *}
     1.5  
     1.6  theory Nat
     1.7 -imports Inductive Product_Type Fields
     1.8 +imports Inductive Typedef Fun Fields
     1.9  uses
    1.10    "~~/src/Tools/rat.ML"
    1.11    "~~/src/Provers/Arith/cancel_sums.ML"