# HG changeset patch
# User paulson
# Date 957958587 -7200
# Node ID 03cb6625c4a5753765f0547ea7708f42353ebfb6
# Parent  f1933a670ae4fe49074ac3ff30c9fb2b4eebe397
new default simprule for better compatibility with old setup

diff -r f1933a670ae4 -r 03cb6625c4a5 src/HOL/Integ/NatSimprocs.ML
--- a/src/HOL/Integ/NatSimprocs.ML	Wed May 10 11:17:01 2000 +0200
+++ b/src/HOL/Integ/NatSimprocs.ML	Wed May 10 13:36:27 2000 +0200
@@ -280,6 +280,15 @@
 Addsimprocs Nat_Numeral_Simprocs.cancel_numerals;
 Addsimprocs [Nat_Numeral_Simprocs.combine_numerals];
 
+
+(*If the result is just #1 + ..., replace it by Suc so that primrecs, etc.
+  will work.*)
+Goal "#1 + n = Suc n";
+by Auto_tac;
+qed "one_plus_eq_Suc";
+Addsimps [one_plus_eq_Suc];
+
+
 (*examples:
 print_depth 22;
 set proof_timing;