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