# HG changeset patch
# User nipkow
# Date 1245858649 -7200
# Node ID d5a6096b94ade986781d0da1148b9d43ed58398e
# Parent  c9a1caf218c886a8097f9cbdafac87f11a844fb9
Replaced Suc_remove by Suc_eq_plus1

diff -r c9a1caf218c8 -r d5a6096b94ad src/HOL/NewNumberTheory/Cong.thy
--- a/src/HOL/NewNumberTheory/Cong.thy	Wed Jun 24 15:51:07 2009 +0200
+++ b/src/HOL/NewNumberTheory/Cong.thy	Wed Jun 24 17:50:49 2009 +0200
@@ -60,9 +60,7 @@
 lemma nat_1' [simp]: "nat 1 = 1"
 by simp
 
-(* For those annoying moments where Suc reappears *)
-lemma Suc_remove: "Suc n = n + 1"
-by simp
+(* For those annoying moments where Suc reappears, use Suc_eq_plus1 *)
 
 declare nat_1 [simp del]
 declare add_2_eq_Suc [simp del] 
diff -r c9a1caf218c8 -r d5a6096b94ad src/HOL/NewNumberTheory/Fib.thy
--- a/src/HOL/NewNumberTheory/Fib.thy	Wed Jun 24 15:51:07 2009 +0200
+++ b/src/HOL/NewNumberTheory/Fib.thy	Wed Jun 24 17:50:49 2009 +0200
@@ -145,7 +145,7 @@
   apply (subst nat_fib_reduce)
   apply (auto simp add: ring_simps)
   apply (subst (1 3 5) nat_fib_reduce)
-  apply (auto simp add: ring_simps Suc_remove)
+  apply (auto simp add: ring_simps Suc_eq_plus1)
 (* hmmm. Why doesn't "n + (1 + (1 + k))" simplify to "n + k + 2"? *)
   apply (subgoal_tac "n + (k + 2) = n + (1 + (1 + k))")
   apply (erule ssubst) back back
@@ -220,7 +220,7 @@
   apply (induct n rule: nat_fib_induct)
   apply auto
   apply (subst (2) nat_fib_reduce)
-  apply (auto simp add: Suc_remove) (* again, natdiff_cancel *)
+  apply (auto simp add: Suc_eq_plus1) (* again, natdiff_cancel *)
   apply (subst add_commute, auto)
   apply (subst nat_gcd_commute, auto simp add: ring_simps)
 done