1.1 --- a/src/HOL/Word/Num_Lemmas.thy	Tue Apr 28 15:50:30 2009 +0200
     1.2 +++ b/src/HOL/Word/Num_Lemmas.thy	Tue Apr 28 15:50:32 2009 +0200
     1.3 @@ -45,10 +45,6 @@
     1.4    apply (simp add: number_of_eq nat_diff_distrib [symmetric])
     1.5    done
     1.6  
     1.7 -lemma of_int_power:
     1.8 -  "of_int (a ^ n) = (of_int a ^ n :: 'a :: {recpower, comm_ring_1})" 
     1.9 -  by (induct n) (auto simp add: power_Suc)
    1.10 -
    1.11  lemma zless2: "0 < (2 :: int)" by arith
    1.12  
    1.13  lemmas zless2p [simp] = zless2 [THEN zero_less_power]