1.1 --- a/src/HOL/Int.thy	Tue Apr 28 13:34:45 2009 +0200
     1.2 +++ b/src/HOL/Int.thy	Tue Apr 28 13:34:46 2009 +0200
     1.3 @@ -1266,14 +1266,9 @@
     1.4  definition Ints  :: "'a set" where
     1.5    [code del]: "Ints = range of_int"
     1.6  
     1.7 -end
     1.8 -
     1.9  notation (xsymbols)
    1.10    Ints  ("\<int>")
    1.11  
    1.12 -context ring_1
    1.13 -begin
    1.14 -
    1.15  lemma Ints_0 [simp]: "0 \<in> \<int>"
    1.16  apply (simp add: Ints_def)
    1.17  apply (rule range_eqI)
    1.18 @@ -1848,15 +1843,10 @@
    1.19  
    1.20  subsection {* Integer Powers *} 
    1.21  
    1.22 -context ring_1
    1.23 -begin
    1.24 -
    1.25  lemma of_int_power:
    1.26    "of_int (z ^ n) = of_int z ^ n"
    1.27    by (induct n) simp_all
    1.28  
    1.29 -end
    1.30 -
    1.31  lemma zpower_zpower:
    1.32    "(x ^ y) ^ z = (x ^ (y * z)::int)"
    1.33    by (rule power_mult [symmetric])