# HG changeset patch
# User paulson
# Date 1142939803 -3600
# Node ID 8f6e097d7b23ab6ac9d6addc8de63205eef5dfd4
# Parent  ad96f1095dca2af636fd599f209ebd69924a859b
Removal of unnecessary simprules: simproc cancel_numerals now works without
add_Suc, while the reason for the horrible isolateSuc is not known.

diff -r ad96f1095dca -r 8f6e097d7b23 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Mon Mar 20 21:29:04 2006 +0100
+++ b/src/HOL/arith_data.ML	Tue Mar 21 12:16:43 2006 +0100
@@ -382,18 +382,12 @@
 
 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_zero_left,add_zero_right,Zero_not_Suc,Suc_not_Zero,le_0_eq,
-  add_Suc, One_nat_def,isolateSuc,
+  One_nat_def,
   order_less_irrefl, zero_neq_one, zero_less_one, zero_le_one,
   zero_neq_one RS not_sym, not_one_le_zero, not_one_less_zero];