# HG changeset patch
# User nipkow
# Date 1234201810 -3600
# Node ID a2baf1b221be07c99e7985e7c811e05d210b2341
# Parent  409138c4de1208a6324214c2b0bc2fd723772da6
new attribute "arith" for facts supplied to arith.

diff -r 409138c4de12 -r a2baf1b221be src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sun Feb 08 11:59:26 2009 +0100
+++ b/src/HOL/Nat.thy	Mon Feb 09 18:50:10 2009 +0100
@@ -1336,12 +1336,19 @@
 use "Tools/arith_data.ML"
 declaration {* K ArithData.setup *}
 
+ML{*
+structure ArithFacts =
+  NamedThmsFun(val name = "arith"
+               val description = "arith facts - only ground formulas");
+*}
+
+setup ArithFacts.setup
+
 use "Tools/lin_arith.ML"
 declaration {* K LinArith.setup *}
 
 lemmas [arith_split] = nat_diff_split split_min split_max
 
-
 context order
 begin
 
diff -r 409138c4de12 -r a2baf1b221be src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Sun Feb 08 11:59:26 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Mon Feb 09 18:50:10 2009 +0100
@@ -814,11 +814,14 @@
       addsimprocs ArithData.nat_cancel_sums_add}) #>
   arith_discrete "nat";
 
-val lin_arith_simproc = Fast_Arith.lin_arith_simproc;
+fun add_arith_facts ss =
+  add_prems (ArithFacts.get (MetaSimplifier.the_context ss)) ss;
+
+val lin_arith_simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc;
 
 val fast_nat_arith_simproc =
   Simplifier.simproc (the_context ()) "fast_nat_arith"
-    ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] (K Fast_Arith.lin_arith_simproc);
+    ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] (K lin_arith_simproc);
 
 (* Because of fast_nat_arith_simproc, the arithmetic solver is really only
 useful to detect inconsistencies among the premises for subgoals which are
@@ -912,7 +915,8 @@
 fun arith_method src =
   Method.syntax Args.bang_facts src
   #> (fn (prems, ctxt) => Method.METHOD (fn facts =>
-      HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac ctxt)));
+      HEADGOAL (Method.insert_tac (prems @ ArithFacts.get ctxt @ facts)
+      THEN' arith_tac ctxt)));
 
 end;