# HG changeset patch
# User haftmann
# Date 1272363609 -7200
# Node ID f3f389fc797454d51b8585114c4449d9fb639ece
# Parent  63fc238a743088f13cdfd352703515d7f82c41b6
got rid of [simplified]

diff -r 63fc238a7430 -r f3f389fc7974 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Tue Apr 27 11:52:41 2010 +0200
+++ b/src/HOL/Int.thy	Tue Apr 27 12:20:09 2010 +0200
@@ -324,27 +324,6 @@
 
 end
 
-context linordered_idom
-begin
-
-lemma of_int_le_iff [simp]:
-  "of_int w \<le> of_int z \<longleftrightarrow> w \<le> z"
-by (cases w, cases z, simp add: of_int le minus algebra_simps of_nat_add [symmetric] del: of_nat_add)
-
-text{*Special cases where either operand is zero*}
-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 \<longleftrightarrow> w < z"
-  by (simp add: not_le [symmetric] linorder_not_le [symmetric])
-
-text{*Special cases where either operand is zero*}
-lemmas of_int_0_less_iff [simp] = of_int_less_iff [of 0, simplified]
-lemmas of_int_less_0_iff [simp] = of_int_less_iff [of _ 0, simplified]
-
-end
-
 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
@@ -358,13 +337,47 @@
 done
 
 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_0_iff [simp]:
+  "of_int z = 0 \<longleftrightarrow> z = 0"
+  using of_int_eq_iff [of z 0] by simp
+
+lemma of_int_0_eq_iff [simp]:
+  "0 = of_int z \<longleftrightarrow> z = 0"
+  using of_int_eq_iff [of 0 z] by simp
 
 end
 
+context linordered_idom
+begin
+
 text{*Every @{text linordered_idom} has characteristic zero.*}
-subclass (in linordered_idom) ring_char_0 by intro_locales
+subclass ring_char_0 ..
+
+lemma of_int_le_iff [simp]:
+  "of_int w \<le> of_int z \<longleftrightarrow> w \<le> z"
+  by (cases w, cases z, simp add: of_int le minus algebra_simps of_nat_add [symmetric] del: of_nat_add)
+
+lemma of_int_less_iff [simp]:
+  "of_int w < of_int z \<longleftrightarrow> w < z"
+  by (simp add: less_le order_less_le)
+
+lemma of_int_0_le_iff [simp]:
+  "0 \<le> of_int z \<longleftrightarrow> 0 \<le> z"
+  using of_int_le_iff [of 0 z] by simp
+
+lemma of_int_le_0_iff [simp]:
+  "of_int z \<le> 0 \<longleftrightarrow> z \<le> 0"
+  using of_int_le_iff [of z 0] by simp
+
+lemma of_int_0_less_iff [simp]:
+  "0 < of_int z \<longleftrightarrow> 0 < z"
+  using of_int_less_iff [of 0 z] by simp
+
+lemma of_int_less_0_iff [simp]:
+  "of_int z < 0 \<longleftrightarrow> z < 0"
+  using of_int_less_iff [of z 0] by simp
+
+end
 
 lemma of_int_eq_id [simp]: "of_int = id"
 proof