1.1 --- a/src/HOL/Fields.thy	Tue Apr 27 10:51:39 2010 +0200
     1.2 +++ b/src/HOL/Fields.thy	Tue Apr 27 11:52:41 2010 +0200
     1.3 @@ -778,15 +778,22 @@
     1.4  done
     1.5  
     1.6  text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*}
     1.7 -lemmas zero_less_divide_1_iff = zero_less_divide_iff [of 1, simplified]
     1.8 -lemmas divide_less_0_1_iff = divide_less_0_iff [of 1, simplified]
     1.9 -lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]
    1.10 -lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]
    1.11  
    1.12 -declare zero_less_divide_1_iff [simp,no_atp]
    1.13 -declare divide_less_0_1_iff [simp,no_atp]
    1.14 -declare zero_le_divide_1_iff [simp,no_atp]
    1.15 -declare divide_le_0_1_iff [simp,no_atp]
    1.16 +lemma zero_le_divide_1_iff [simp, no_atp]:
    1.17 +  "0 \<le> 1 / a \<longleftrightarrow> 0 \<le> a"
    1.18 +  by (simp add: zero_le_divide_iff)
    1.19 +
    1.20 +lemma zero_less_divide_1_iff [simp, no_atp]:
    1.21 +  "0 < 1 / a \<longleftrightarrow> 0 < a"
    1.22 +  by (simp add: zero_less_divide_iff)
    1.23 +
    1.24 +lemma divide_le_0_1_iff [simp, no_atp]:
    1.25 +  "1 / a \<le> 0 \<longleftrightarrow> a \<le> 0"
    1.26 +  by (simp add: divide_le_0_iff)
    1.27 +
    1.28 +lemma divide_less_0_1_iff [simp, no_atp]:
    1.29 +  "1 / a < 0 \<longleftrightarrow> a < 0"
    1.30 +  by (simp add: divide_less_0_iff)
    1.31  
    1.32  lemma divide_right_mono:
    1.33       "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/c"
    1.34 @@ -805,7 +812,6 @@
    1.35  done
    1.36  
    1.37  
    1.38 -
    1.39  text{*Simplify quotients that are compared with the value 1.*}
    1.40  
    1.41  lemma le_divide_eq_1 [no_atp]: