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

diff -r 69004340f53c -r 63fc238a7430 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Tue Apr 27 10:51:39 2010 +0200
+++ b/src/HOL/Fields.thy	Tue Apr 27 11:52:41 2010 +0200
@@ -778,15 +778,22 @@
 done
 
 text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*}
-lemmas zero_less_divide_1_iff = zero_less_divide_iff [of 1, simplified]
-lemmas divide_less_0_1_iff = divide_less_0_iff [of 1, simplified]
-lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]
-lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]
+
+lemma zero_le_divide_1_iff [simp, no_atp]:
+  "0 \<le> 1 / a \<longleftrightarrow> 0 \<le> a"
+  by (simp add: zero_le_divide_iff)
 
-declare zero_less_divide_1_iff [simp,no_atp]
-declare divide_less_0_1_iff [simp,no_atp]
-declare zero_le_divide_1_iff [simp,no_atp]
-declare divide_le_0_1_iff [simp,no_atp]
+lemma zero_less_divide_1_iff [simp, no_atp]:
+  "0 < 1 / a \<longleftrightarrow> 0 < a"
+  by (simp add: zero_less_divide_iff)
+
+lemma divide_le_0_1_iff [simp, no_atp]:
+  "1 / a \<le> 0 \<longleftrightarrow> a \<le> 0"
+  by (simp add: divide_le_0_iff)
+
+lemma divide_less_0_1_iff [simp, no_atp]:
+  "1 / a < 0 \<longleftrightarrow> a < 0"
+  by (simp add: divide_less_0_iff)
 
 lemma divide_right_mono:
      "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/c"
@@ -805,7 +812,6 @@
 done
 
 
-
 text{*Simplify quotients that are compared with the value 1.*}
 
 lemma le_divide_eq_1 [no_atp]: