diff -r 771117253634 -r 25ca91279a9b src/HOL/Library/Parity.thy
--- a/src/HOL/Library/Parity.thy	Wed Jun 20 05:06:56 2007 +0200
+++ b/src/HOL/Library/Parity.thy	Wed Jun 20 05:18:39 2007 +0200
@@ -20,7 +20,7 @@
   even_def: "even x \<equiv> x mod 2 = 0" ..
 
 instance nat :: even_odd
-  even_nat_def: "even x \<equiv> even (int_of_nat x)" ..
+  even_nat_def: "even x \<equiv> even (int x)" ..
 
 
 subsection {* Even and odd are mutually exclusive *}
@@ -135,7 +135,7 @@
   by (simp add: even_nat_def)
 
 lemma even_nat_product: "even((x::nat) * y) = (even x | even y)"
-  by (simp add: even_nat_def)
+  by (simp add: even_nat_def int_mult)
 
 lemma even_nat_sum: "even ((x::nat) + y) =
     ((even x & even y) | (odd x & odd y))"
@@ -152,7 +152,7 @@
   by (simp add: even_nat_def)
 
 lemma even_nat_power: "even ((x::nat)^y) = (even x & 0 < y)"
-  by (simp add: even_nat_def of_nat_power)
+  by (simp add: even_nat_def int_power)
 
 lemma even_nat_zero: "even (0::nat)"
   by (simp add: even_nat_def)