# HG changeset patch
# User oheimb
# Date 982691245 -3600
# Node ID 03f5dc539fd9e889e940069dded6ede2eb784602
# Parent  14732e3eaa6e4adb6a19d505ea166b85179a7ddc
added add_arith (just as hint by now)

diff -r 14732e3eaa6e -r 03f5dc539fd9 src/HOL/NatArith.thy
--- a/src/HOL/NatArith.thy	Tue Feb 20 18:47:22 2001 +0100
+++ b/src/HOL/NatArith.thy	Tue Feb 20 18:47:25 2001 +0100
@@ -14,8 +14,14 @@
     "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
   by (cases "a < b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2])
 
-ML {* val nat_diff_split = thm "nat_diff_split" *}
+ML {*
+ val nat_diff_split = thm "nat_diff_split";
+
+(* TODO: use this for force_tac in Provers/clasip.ML *)
+fun add_arith cs = cs addaltern ("arith_tac", arith_tac);
+*}
 
 lemmas [arith_split] = nat_diff_split split_min split_max
 
+
 end