--- 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]
--- 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