# HG changeset patch
# User nipkow
# Date 1142631186 -3600
# Node ID dac2c80142532a90b649a2e42effdecb1c583437
# Parent  4c86109423d5ace3ea70eec9f5a56bc2d89dc995
fixed problem with proof reconstruction by adding add_Suc to arith-simpset.

diff -r 4c86109423d5 -r dac2c8014253 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Fri Mar 17 17:38:38 2006 +0100
+++ b/src/HOL/arith_data.ML	Fri Mar 17 22:33:06 2006 +0100
@@ -393,7 +393,7 @@
 *)
 val add_rules =
  [add_zero_left,add_zero_right,Zero_not_Suc,Suc_not_Zero,le_0_eq,
-  One_nat_def,isolateSuc,
+  add_Suc, One_nat_def,isolateSuc,
   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];