# HG changeset patch
# User haftmann
# Date 1240918486 -7200
# Node ID aabad7789183edf88750f93fe456aaea21d13fc1
# Parent  41fd307cab30c11e88b21f6c1830bed03c32e04f
local syntax for Ints; ephermal re-globalization

diff -r 41fd307cab30 -r aabad7789183 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Tue Apr 28 13:34:45 2009 +0200
+++ b/src/HOL/Int.thy	Tue Apr 28 13:34:46 2009 +0200
@@ -1266,14 +1266,9 @@
 definition Ints  :: "'a set" where
   [code del]: "Ints = range of_int"
 
-end
-
 notation (xsymbols)
   Ints  ("\<int>")
 
-context ring_1
-begin
-
 lemma Ints_0 [simp]: "0 \<in> \<int>"
 apply (simp add: Ints_def)
 apply (rule range_eqI)
@@ -1848,15 +1843,10 @@
 
 subsection {* Integer Powers *} 
 
-context ring_1
-begin
-
 lemma of_int_power:
   "of_int (z ^ n) = of_int z ^ n"
   by (induct n) simp_all
 
-end
-
 lemma zpower_zpower:
   "(x ^ y) ^ z = (x ^ (y * z)::int)"
   by (rule power_mult [symmetric])