# HG changeset patch
# User wenzelm
# Date 1185903622 -7200
# Node ID 109f19a13872862dc99ca5dfbc11dfce2c4823a7
# Parent  ab6f0480700526353d1efdf3202d50821c9efa00
added Tools/lin_arith.ML;

diff -r ab6f04807005 -r 109f19a13872 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Jul 31 19:38:33 2007 +0200
+++ b/src/HOL/IsaMakefile	Tue Jul 31 19:40:22 2007 +0200
@@ -119,7 +119,7 @@
   Tools/function_package/mutual.ML					\
   Tools/function_package/pattern_split.ML Tools/inductive_codegen.ML	\
   Tools/inductive_package.ML Tools/inductive_realizer.ML		\
-  Tools/inductive_set_package.ML Tools/meson.ML				\
+  Tools/inductive_set_package.ML Tools/lin_arith.ML Tools/meson.ML	\
   Tools/metis_tools.ML Tools/numeral.ML Tools/numeral_syntax.ML		\
   Tools/polyhash.ML Tools/primrec_package.ML Tools/prop_logic.ML 	\
   Tools/recdef_package.ML Tools/recfun_codegen.ML			\
diff -r ab6f04807005 -r 109f19a13872 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Jul 31 19:38:33 2007 +0200
+++ b/src/HOL/Nat.thy	Tue Jul 31 19:40:22 2007 +0200
@@ -12,9 +12,10 @@
 imports Wellfounded_Recursion Ring_and_Field
 uses
   "~~/src/Tools/rat.ML"
-  "~~/src/Provers/Arith/fast_lin_arith.ML"
   "~~/src/Provers/Arith/cancel_sums.ML"
   ("arith_data.ML")
+  "~~/src/Provers/Arith/fast_lin_arith.ML"
+  ("Tools/lin_arith.ML")
 begin
 
 subsection {* Type @{text ind} *}
@@ -1092,7 +1093,11 @@
   using 2 1 by (rule trans)
 
 use "arith_data.ML"
-declaration {* K arith_setup *}
+declaration {* K arith_data_setup *}
+
+use "Tools/lin_arith.ML"
+declaration {* K LinArith.setup *}
+
 
 text{*The following proofs may rely on the arithmetic proof procedures.*}