
diff -r a5f1e4f46d14 -r 7cdcc9dd95cb src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu Mar 12 18:01:25 2009 +0100
+++ b/src/HOL/Nat.thy	Thu Mar 12 18:01:26 2009 +0100
@@ -2,7 +2,7 @@
     Author:     Tobias Nipkow and Lawrence C Paulson and Markus Wenzel
 
 Type "nat" is a linear order, and a datatype; arithmetic operators + -
-and * (for div, mod and dvd, see theory Divides).
+and * (for div and mod, see theory Divides).
 *)
 
 header {* Natural numbers *}
@@ -12,7 +12,8 @@
 uses
   "~~/src/Tools/rat.ML"
   "~~/src/Provers/Arith/cancel_sums.ML"
-  ("Tools/arith_data.ML")
+  "Tools/arith_data.ML"
+  ("Tools/nat_arith.ML")
   "~~/src/Provers/Arith/fast_lin_arith.ML"
   ("Tools/lin_arith.ML")
 begin
@@ -1344,8 +1345,8 @@
   shows "u = s"
   using 2 1 by (rule trans)
 
-use "Tools/arith_data.ML"
-declaration {* K ArithData.setup *}
+use "Tools/nat_arith.ML"
+declaration {* K Nat_Arith.setup *}
 
 ML{*
 structure ArithFacts =




