# HG changeset patch
# User haftmann
# Date 1240926632 -7200
# Node ID b8a8cf6e16f212995db33a331b9dbbf2f616ed23
# Parent  2c227493ea566caaa81a371fbd94ead78014c08e
stripped lemma duplicatesrc/HOL/Word/Num_Lemmas.thy

diff -r 2c227493ea56 -r b8a8cf6e16f2 src/HOL/Word/Num_Lemmas.thy
--- a/src/HOL/Word/Num_Lemmas.thy	Tue Apr 28 15:50:30 2009 +0200
+++ b/src/HOL/Word/Num_Lemmas.thy	Tue Apr 28 15:50:32 2009 +0200
@@ -45,10 +45,6 @@
   apply (simp add: number_of_eq nat_diff_distrib [symmetric])
   done
 
-lemma of_int_power:
-  "of_int (a ^ n) = (of_int a ^ n :: 'a :: {recpower, comm_ring_1})" 
-  by (induct n) (auto simp add: power_Suc)
-
 lemma zless2: "0 < (2 :: int)" by arith
 
 lemmas zless2p [simp] = zless2 [THEN zero_less_power]