| changeset 23438 | dd824e86fa8a |
| parent 23431 | 25ca91279a9b |
| child 23477 | f4b83f03cac9 |
--- a/src/HOL/IntDef.thy Wed Jun 20 17:02:57 2007 +0200 +++ b/src/HOL/IntDef.thy Wed Jun 20 17:28:55 2007 +0200 @@ -554,7 +554,8 @@ qed lemma of_nat_nat: "0 \<le> z ==> of_nat (nat z) = of_int z" -by (cases z rule: eq_Abs_Integ, simp add: nat le of_int Zero_int_def) +by (cases z rule: eq_Abs_Integ) + (simp add: nat le of_int Zero_int_def of_nat_diff) subsection{*The Set of Integers*}