diff -r b8da286bb9ad -r dfc2654eea9f src/HOL/Integ/IntDiv.thy
--- a/src/HOL/Integ/IntDiv.thy	Wed Nov 24 08:43:41 2004 +0100
+++ b/src/HOL/Integ/IntDiv.thy	Wed Nov 24 10:23:36 2004 +0100
@@ -1195,6 +1195,9 @@
 apply (auto simp add: zero_le_mult_iff)
 done
 
+theorem zpower_int: "(int m)^n = int (m^n)"
+  by (induct n) (simp_all add: zmult_int)
+
 lemma zdiv_int: "int (a div b) = (int a) div (int b)"
 apply (subst split_div, auto)
 apply (subst split_zdiv, auto)
@@ -1317,6 +1320,7 @@
 val zpower_zpower = thm "zpower_zpower";
 val zero_less_zpower_abs_iff = thm "zero_less_zpower_abs_iff";
 val zero_le_zpower_abs = thm "zero_le_zpower_abs";
+val zpower_int = thm "zpower_int";
 *}
 
 end