# HG changeset patch
# User wenzelm
# Date 933334977 -7200
# Node ID 0b2fe9ec709cdafa8e0ad5120fcc3b2bd36d6517
# Parent  a17f7b5ac40f3ae2813f686de1abffa53f5c80e3
'arith' proof method;

diff -r a17f7b5ac40f -r 0b2fe9ec709c src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Fri Jul 30 13:41:43 1999 +0200
+++ b/src/HOL/Arith.ML	Fri Jul 30 13:42:57 1999 +0200
@@ -1003,6 +1003,15 @@
   refute_tac (K true) (REPEAT o split_tac[nat_diff_split,split_min,split_max])
              ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac);
 
+
+(* proof method setup *)
+
+val arith_method = Method.METHOD (fn facts => FIRSTGOAL (Method.same_tac facts THEN' arith_tac));
+
+val arith_setup =
+ [Method.add_methods
+  [("arith", Method.no_args arith_method, "decide linear arithmethic")]];
+
 (*---------------------------------------------------------------------------*)
 (* End of proof procedures. Now go and USE them!                             *)
 (*---------------------------------------------------------------------------*)
diff -r a17f7b5ac40f -r 0b2fe9ec709c src/HOL/Univ.thy
--- a/src/HOL/Univ.thy	Fri Jul 30 13:41:43 1999 +0200
+++ b/src/HOL/Univ.thy	Fri Jul 30 13:42:57 1999 +0200
@@ -11,6 +11,9 @@
 
 Univ = Arith + Sum +
 
+setup arith_setup
+
+
 (** lists, trees will be sets of nodes **)
 
 global