diff -r 458e55fd0a33 -r fec1a04b7220 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/Int.thy	Wed Apr 22 19:09:21 2009 +0200
@@ -1848,42 +1848,18 @@
 
 subsection {* Integer Powers *} 
 
-instantiation int :: recpower
-begin
-
-primrec power_int where
-  "p ^ 0 = (1\<Colon>int)"
-  | "p ^ (Suc n) = (p\<Colon>int) * (p ^ n)"
-
-instance proof
-  fix z :: int
-  fix n :: nat
-  show "z ^ 0 = 1" by simp
-  show "z ^ Suc n = z * (z ^ n)" by simp
-qed
-
-declare power_int.simps [simp del]
-
-end
-
-lemma zpower_zadd_distrib: "x ^ (y + z) = ((x ^ y) * (x ^ z)::int)"
-  by (rule Power.power_add)
-
-lemma zpower_zpower: "(x ^ y) ^ z = (x ^ (y * z)::int)"
-  by (rule Power.power_mult [symmetric])
-
-lemma zero_less_zpower_abs_iff [simp]:
-  "(0 < abs x ^ n) \<longleftrightarrow> (x \<noteq> (0::int) | n = 0)"
-  by (induct n) (auto simp add: zero_less_mult_iff)
-
-lemma zero_le_zpower_abs [simp]: "(0::int) \<le> abs x ^ n"
-  by (induct n) (auto simp add: zero_le_mult_iff)
+instance int :: recpower ..
 
 lemma of_int_power:
   "of_int (z ^ n) = (of_int z ^ n :: 'a::{recpower, ring_1})"
   by (induct n) simp_all
 
-lemma int_power: "int (m^n) = (int m) ^ n"
+lemma zpower_zpower:
+  "(x ^ y) ^ z = (x ^ (y * z)::int)"
+  by (rule power_mult [symmetric])
+
+lemma int_power:
+  "int (m^n) = (int m) ^ n"
   by (rule of_nat_power)
 
 lemmas zpower_int = int_power [symmetric]
@@ -2278,4 +2254,15 @@
 lemmas zless_le = less_int_def
 lemmas int_eq_of_nat = TrueI
 
+lemma zpower_zadd_distrib:
+  "x ^ (y + z) = ((x ^ y) * (x ^ z)::int)"
+  by (rule power_add)
+
+lemma zero_less_zpower_abs_iff:
+  "(0 < abs x ^ n) \<longleftrightarrow> (x \<noteq> (0::int) | n = 0)"
+  by (rule zero_less_power_abs_iff)
+
+lemma zero_le_zpower_abs: "(0::int) \<le> abs x ^ n"
+  by (rule zero_le_power_abs)
+
 end