1.1 --- a/src/HOL/Int.thy	Tue Apr 28 15:50:29 2009 +0200
     1.2 +++ b/src/HOL/Int.thy	Tue Apr 28 15:50:29 2009 +0200
     1.3 @@ -292,9 +292,7 @@
     1.4  context ring_1
     1.5  begin
     1.6  
     1.7 -definition
     1.8 -  of_int :: "int \<Rightarrow> 'a"
     1.9 -where
    1.10 +definition of_int :: "int \<Rightarrow> 'a" where
    1.11    [code del]: "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
    1.12  
    1.13  lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
    1.14 @@ -330,6 +328,10 @@
    1.15  lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n"
    1.16  by (induct n) auto
    1.17  
    1.18 +lemma of_int_power:
    1.19 +  "of_int (z ^ n) = of_int z ^ n"
    1.20 +  by (induct n) simp_all
    1.21 +
    1.22  end
    1.23  
    1.24  context ordered_idom
    1.25 @@ -1841,23 +1843,6 @@
    1.26  qed
    1.27  
    1.28  
    1.29 -subsection {* Integer Powers *} 
    1.30 -
    1.31 -lemma of_int_power:
    1.32 -  "of_int (z ^ n) = of_int z ^ n"
    1.33 -  by (induct n) simp_all
    1.34 -
    1.35 -lemma zpower_zpower:
    1.36 -  "(x ^ y) ^ z = (x ^ (y * z)::int)"
    1.37 -  by (rule power_mult [symmetric])
    1.38 -
    1.39 -lemma int_power:
    1.40 -  "int (m ^ n) = int m ^ n"
    1.41 -  by (rule of_nat_power)
    1.42 -
    1.43 -lemmas zpower_int = int_power [symmetric]
    1.44 -
    1.45 -
    1.46  subsection {* Further theorems on numerals *}
    1.47  
    1.48  subsubsection{*Special Simplification for Constants*}
    1.49 @@ -2260,4 +2245,14 @@
    1.50  lemma zero_le_zpower_abs: "(0::int) \<le> abs x ^ n"
    1.51    by (rule zero_le_power_abs)
    1.52  
    1.53 +lemma zpower_zpower:
    1.54 +  "(x ^ y) ^ z = (x ^ (y * z)::int)"
    1.55 +  by (rule power_mult [symmetric])
    1.56 +
    1.57 +lemma int_power:
    1.58 +  "int (m ^ n) = int m ^ n"
    1.59 +  by (rule of_nat_power)
    1.60 +
    1.61 +lemmas zpower_int = int_power [symmetric]
    1.62 +
    1.63  end