diff -r 5a989586d102 -r df8b5c05546f src/HOL/Nat_Numeral.thy
--- a/src/HOL/Nat_Numeral.thy	Thu Oct 29 22:13:11 2009 +0100
+++ b/src/HOL/Nat_Numeral.thy	Thu Oct 29 22:16:12 2009 +0100
@@ -420,10 +420,6 @@
 
 subsubsection{*Equals (=) *}
 
-lemma eq_nat_nat_iff:
-     "[| (0::int) <= z;  0 <= z' |] ==> (nat z = nat z') = (z=z')"
-by (auto elim!: nonneg_eq_int)
-
 lemma eq_nat_number_of [simp]:
      "((number_of v :: nat) = number_of v') =  
       (if neg (number_of v :: int) then (number_of v' :: int) \<le> 0
@@ -625,11 +621,6 @@
  
 subsection{*Literal arithmetic involving powers*}
 
-lemma nat_power_eq: "(0::int) <= z ==> nat (z^n) = nat z ^ n"
-apply (induct "n")
-apply (simp_all (no_asm_simp) add: nat_mult_distrib)
-done
-
 lemma power_nat_number_of:
      "(number_of v :: nat) ^ n =  
        (if neg (number_of v :: int) then 0^n else nat ((number_of v :: int) ^ n))"