changeset 33056 | 791a4655cae3 |
parent 32437 | 66f1a0dfe7d9 |
child 33296 | a3924d1069e5 |
--- a/src/HOL/Int.thy Wed Oct 21 16:57:57 2009 +0200 +++ b/src/HOL/Int.thy Wed Oct 21 17:34:35 2009 +0200 @@ -1614,7 +1614,7 @@ context ring_1 begin -lemma of_int_of_nat [nitpick_const_simp]: +lemma of_int_of_nat [nitpick_simp]: "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))" proof (cases "k < 0") case True then have "0 \<le> - k" by simp