# HG changeset patch
# User huffman
# Date 1187722270 -7200
# Node ID b57c48f7e2d48077838c480ef3c03f0f5f0873b1
# Parent  9b5073c79a0bad87e1fa7900682ef7ae378b1cea
add lemma of_int_power

diff -r 9b5073c79a0b -r b57c48f7e2d4 src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Tue Aug 21 20:50:12 2007 +0200
+++ b/src/HOL/IntDiv.thy	Tue Aug 21 20:51:10 2007 +0200
@@ -1357,6 +1357,9 @@
   show "z^(Suc n) = z * (z^n)" by simp
 qed
 
+lemma of_int_power:
+  "of_int (z ^ n) = (of_int z ^ n :: 'a::{recpower, ring_1})"
+  by (induct n) (simp_all add: power_Suc)
 
 lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
 apply (induct "y", auto)