# 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.*}