# HG changeset patch
# User nipkow
# Date 1049689878 -7200
# Node ID b41fc9a31975a1071367e93efb21f65b02066b58
# Parent  af38553e61ee3acd88b94ab9f88671d6047adc0f
added isolate_Suc to counteract deficiencies in one of Larry's simprocs.

diff -r af38553e61ee -r b41fc9a31975 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Sun Apr 06 21:16:50 2003 +0200
+++ b/src/HOL/arith_data.ML	Mon Apr 07 06:31:18 2003 +0200
@@ -367,12 +367,18 @@
 
 local
 
+val isolateSuc =
+  let val thy = theory "Nat"
+  in prove_goal thy "Suc(i+j) = i+j + Suc 0"
+     (fn _ => [simp_tac (simpset_of thy) 1])
+  end;
+
 (* reduce contradictory <= to False.
    Most of the work is done by the cancel tactics.
 *)
 val add_rules =
  [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq,
-  One_nat_def];
+  One_nat_def,isolateSuc];
 
 val add_mono_thms_nat = map (fn s => prove_goal (the_context ()) s
  (fn prems => [cut_facts_tac prems 1,