| changeset 44766 | d4d33a4d7548 |
| parent 44345 | 881c324470a2 |
| child 44857 | 73d5b722c4b4 |
--- a/src/HOL/Nat_Numeral.thy Tue Sep 06 16:30:39 2011 -0700 +++ b/src/HOL/Nat_Numeral.thy Tue Sep 06 19:03:41 2011 -0700 @@ -364,7 +364,7 @@ lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)" apply (rule sym) -apply (simp add: nat_eq_iff int_Suc) +apply (simp add: nat_eq_iff) done lemma Suc_nat_number_of_add: