--- 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)