diff -r b568f8c5d5ca -r e2e1a4b00de3 src/HOL/IntDef.thy
--- a/src/HOL/IntDef.thy	Thu Oct 25 16:57:57 2007 +0200
+++ b/src/HOL/IntDef.thy	Thu Oct 25 19:27:50 2007 +0200
@@ -426,8 +426,11 @@
 
 subsection{*Embedding of the Integers into any @{text ring_1}: @{term of_int}*}
 
+context ring_1
+begin
+
 definition
-  of_int :: "int \<Rightarrow> 'a\<Colon>ring_1"
+  of_int :: "int \<Rightarrow> 'a"
 where
   "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
 lemmas [code func del] = of_int_def
@@ -453,15 +456,21 @@
 lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)"
 by (cases z, simp add: compare_rls of_int minus)
 
-lemma of_int_diff [simp]: "of_int (w-z) = of_int w - of_int z"
-by (simp add: diff_minus)
-
 lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
 apply (cases w, cases z)
 apply (simp add: compare_rls of_int left_diff_distrib right_diff_distrib
                  mult add_ac of_nat_mult)
 done
 
+text{*Collapse nested embeddings*}
+lemma of_int_of_nat_eq [simp]: "of_int (Nat.of_nat n) = of_nat n"
+  by (induct n, auto)
+
+end
+
+lemma of_int_diff [simp]: "of_int (w-z) = of_int w - of_int z"
+by (simp add: diff_minus)
+
 lemma of_int_le_iff [simp]:
      "(of_int w \<le> (of_int z::'a::ordered_idom)) = (w \<le> z)"
 apply (cases w)
@@ -474,7 +483,6 @@
 lemmas of_int_0_le_iff [simp] = of_int_le_iff [of 0, simplified]
 lemmas of_int_le_0_iff [simp] = of_int_le_iff [of _ 0, simplified]
 
-
 lemma of_int_less_iff [simp]:
      "(of_int w < (of_int z::'a::ordered_idom)) = (w < z)"
 by (simp add: linorder_not_le [symmetric])
@@ -486,83 +494,83 @@
 text{*Class for unital rings with characteristic zero.
  Includes non-ordered rings like the complex numbers.*}
 class ring_char_0 = ring_1 + semiring_char_0
+begin
 
 lemma of_int_eq_iff [simp]:
-   "of_int w = (of_int z \<Colon> 'a\<Colon>ring_char_0) \<longleftrightarrow> w = z"
+   "of_int w = of_int z \<longleftrightarrow> w = z"
 apply (cases w, cases z, simp add: of_int)
 apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq)
 apply (simp only: of_nat_add [symmetric] of_nat_eq_iff)
 done
 
-text{*Every @{text ordered_idom} has characteristic zero.*}
-instance ordered_idom < ring_char_0 ..
-
 text{*Special cases where either operand is zero*}
 lemmas of_int_0_eq_iff [simp] = of_int_eq_iff [of 0, simplified]
 lemmas of_int_eq_0_iff [simp] = of_int_eq_iff [of _ 0, simplified]
 
-lemma of_int_eq_id [simp]: "of_int = (id :: int => int)"
+end
+
+text{*Every @{text ordered_idom} has characteristic zero.*}
+instance ordered_idom \<subseteq> ring_char_0 ..
+
+lemma of_int_eq_id [simp]: "of_int = id"
 proof
-  fix z
-  show "of_int z = id z"
-    by (cases z)
-      (simp add: of_int add minus int_def diff_minus)
+  fix z show "of_int z = id z"
+    by (cases z) (simp add: of_int add minus int_def diff_minus)
 qed
 
-lemma of_nat_nat: "0 \<le> z ==> of_nat (nat z) = of_int z"
+lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z"
 by (cases z rule: eq_Abs_Integ)
    (simp add: nat le of_int Zero_int_def of_nat_diff)
 
 
 subsection{*The Set of Integers*}
 
-constdefs
-  Ints  :: "'a::ring_1 set"
-  "Ints == range of_int"
+context ring_1
+begin
+
+definition
+  Ints  :: "'a set"
+where
+  "Ints = range of_int"
+
+end
 
 notation (xsymbols)
   Ints  ("\<int>")
 
-lemma Ints_0 [simp]: "0 \<in> Ints"
+context ring_1
+begin
+
+lemma Ints_0 [simp]: "0 \<in> \<int>"
 apply (simp add: Ints_def)
 apply (rule range_eqI)
 apply (rule of_int_0 [symmetric])
 done
 
-lemma Ints_1 [simp]: "1 \<in> Ints"
+lemma Ints_1 [simp]: "1 \<in> \<int>"
 apply (simp add: Ints_def)
 apply (rule range_eqI)
 apply (rule of_int_1 [symmetric])
 done
 
-lemma Ints_add [simp]: "[|a \<in> Ints; b \<in> Ints|] ==> a+b \<in> Ints"
+lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>"
 apply (auto simp add: Ints_def)
 apply (rule range_eqI)
 apply (rule of_int_add [symmetric])
 done
 
-lemma Ints_minus [simp]: "a \<in> Ints ==> -a \<in> Ints"
+lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> -a \<in> \<int>"
 apply (auto simp add: Ints_def)
 apply (rule range_eqI)
 apply (rule of_int_minus [symmetric])
 done
 
-lemma Ints_diff [simp]: "[|a \<in> Ints; b \<in> Ints|] ==> a-b \<in> Ints"
-apply (auto simp add: Ints_def)
-apply (rule range_eqI)
-apply (rule of_int_diff [symmetric])
-done
-
-lemma Ints_mult [simp]: "[|a \<in> Ints; b \<in> Ints|] ==> a*b \<in> Ints"
+lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>"
 apply (auto simp add: Ints_def)
 apply (rule range_eqI)
 apply (rule of_int_mult [symmetric])
 done
 
-text{*Collapse nested embeddings*}
-lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n"
-by (induct n, auto)
-
 lemma Ints_cases [cases set: Ints]:
   assumes "q \<in> \<int>"
   obtains (of_int) z where "q = of_int z"
@@ -574,9 +582,17 @@
 qed
 
 lemma Ints_induct [case_names of_int, induct set: Ints]:
-  "q \<in> \<int> ==> (!!z. P (of_int z)) ==> P q"
+  "q \<in> \<int> \<Longrightarrow> (\<And>z. P (of_int z)) \<Longrightarrow> P q"
   by (rule Ints_cases) auto
 
+end
+
+lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a-b \<in> \<int>"
+apply (auto simp add: Ints_def)
+apply (rule range_eqI)
+apply (rule of_int_diff [symmetric])
+done
+
 
 subsection {* @{term setsum} and @{term setprod} *}