--- a/src/HOL/Nat.thy Wed Dec 03 09:53:58 2008 +0100
+++ b/src/HOL/Nat.thy Wed Dec 03 15:58:44 2008 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Nat.thy
- ID: $Id$
Author: Tobias Nipkow and Lawrence C Paulson and Markus Wenzel
Type "nat" is a linear order, and a datatype; arithmetic operators + -
@@ -13,7 +12,7 @@
uses
"~~/src/Tools/rat.ML"
"~~/src/Provers/Arith/cancel_sums.ML"
- ("arith_data.ML")
+ ("Tools/arith_data.ML")
"~~/src/Provers/Arith/fast_lin_arith.ML"
("Tools/lin_arith.ML")
begin
@@ -1323,7 +1322,7 @@
shows "u = s"
using 2 1 by (rule trans)
-use "arith_data.ML"
+use "Tools/arith_data.ML"
declaration {* K ArithData.setup *}
use "Tools/lin_arith.ML"