# HG changeset patch
# User blanchet
# Date 1234812803 -3600
# Node ID 61837a9bdd74e365be36f5c9e2015813e64ed7cf
# Parent  66c5cc1e60a9c72d4a5b41db629a9a24dc491d34
Added Nitpick tag to 'of_int_of_nat'.
This theorem leads to a more efficient encoding to Kodkod than the definition of 'of_int'.

diff -r 66c5cc1e60a9 -r 61837a9bdd74 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Mon Feb 16 10:15:43 2009 +0100
+++ b/src/HOL/Int.thy	Mon Feb 16 20:33:23 2009 +0100
@@ -1627,7 +1627,7 @@
 context ring_1
 begin
 
-lemma of_int_of_nat:
+lemma of_int_of_nat [nitpick_const_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