| changeset 31792 | d5a6096b94ad |
| parent 31719 | 29f5b20e8ee8 |
| child 31952 | 40501bb2d57c |
--- 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]