# 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 \ 1 / a \ 0 \ 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 \ 0 < a" + by (simp add: zero_less_divide_iff) + +lemma divide_le_0_1_iff [simp, no_atp]: + "1 / a \ 0 \ a \ 0" + by (simp add: divide_le_0_iff) + +lemma divide_less_0_1_iff [simp, no_atp]: + "1 / a < 0 \ a < 0" + by (simp add: divide_less_0_iff) lemma divide_right_mono: "[|a \ b; 0 \ c|] ==> a/c \ b/c" @@ -805,7 +812,6 @@ done - text{*Simplify quotients that are compared with the value 1.*} lemma le_divide_eq_1 [no_atp]: