--- 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))"