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