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