diff -r a7f85074c169 -r 30a1692557b0 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Sun Apr 01 09:12:03 2012 +0200
+++ b/src/HOL/Int.thy	Sun Apr 01 16:09:58 2012 +0200
@@ -990,6 +990,8 @@
   "numeral v - (1::nat) = nat (numeral v - 1)"
   using diff_nat_numeral [of v Num.One] by simp
 
+lemmas nat_arith = diff_nat_numeral
+
 
 subsection "Induction principles for int"
 
@@ -1756,6 +1758,8 @@
 lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m"] for m
 lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
 lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
+lemmas zpower_numeral_even = power_numeral_even [where 'a=int]
+lemmas zpower_numeral_odd = power_numeral_odd [where 'a=int]
 
 lemma zpower_zpower:
   "(x ^ y) ^ z = (x ^ (y * z)::int)"