src/HOL/Int.thy
 changeset 31001 7e6ffd8f51a9 parent 30960 fec1a04b7220 child 31010 aabad7789183
```     1.1 --- a/src/HOL/Int.thy	Mon Apr 27 08:22:37 2009 +0200
1.2 +++ b/src/HOL/Int.thy	Mon Apr 27 10:11:44 2009 +0200
1.3 @@ -1536,7 +1536,7 @@
1.5
1.6  lemma abs_power_minus_one [simp]:
1.7 -     "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring,recpower})"
1.8 +  "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring})"
1.10
1.11  lemma of_int_number_of_eq [simp]:
1.12 @@ -1848,18 +1848,21 @@
1.13
1.14  subsection {* Integer Powers *}
1.15
1.16 -instance int :: recpower ..
1.17 +context ring_1
1.18 +begin
1.19
1.20  lemma of_int_power:
1.21 -  "of_int (z ^ n) = (of_int z ^ n :: 'a::{recpower, ring_1})"
1.22 +  "of_int (z ^ n) = of_int z ^ n"
1.23    by (induct n) simp_all
1.24
1.25 +end
1.26 +
1.27  lemma zpower_zpower:
1.28    "(x ^ y) ^ z = (x ^ (y * z)::int)"
1.29    by (rule power_mult [symmetric])
1.30
1.31  lemma int_power:
1.32 -  "int (m^n) = (int m) ^ n"
1.33 +  "int (m ^ n) = int m ^ n"
1.34    by (rule of_nat_power)
1.35
1.36  lemmas zpower_int = int_power [symmetric]
1.37 @@ -2200,6 +2203,8 @@
1.38
1.39  subsection {* Legacy theorems *}
1.40
1.41 +instance int :: recpower ..
1.42 +
1.43  lemmas zminus_zminus = minus_minus [of "z::int", standard]
1.44  lemmas zminus_0 = minus_zero [where 'a=int]