'arith' proof method;

--- 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!                             *)
 (*---------------------------------------------------------------------------*)

--- 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