1.1 --- a/src/HOL/Ring_and_Field.thy	Thu Feb 19 10:41:32 2004 +0100
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Thu Feb 19 15:57:34 2004 +0100
     1.3 @@ -1526,6 +1526,7 @@
     1.4  by (simp add: abs_if linorder_neq_iff)
     1.5  
     1.6  lemma abs_not_less_zero [simp]: "~ abs a < (0::'a::ordered_ring)"
     1.7 +apply (simp add: abs_if)
     1.8  by (simp add: abs_if  order_less_not_sym [of a 0])
     1.9  
    1.10  lemma abs_le_zero_iff [simp]: "(abs a \<le> (0::'a::ordered_ring)) = (a = 0)" 
    1.11 @@ -1620,11 +1621,17 @@
    1.12  
    1.13  lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::ordered_ring))" 
    1.14  apply (simp add: order_less_le abs_le_iff)  
    1.15 +apply (auto simp add: abs_if minus_le_self_iff eq_minus_self_iff)
    1.16 +apply (simp add: le_minus_self_iff linorder_neq_iff) 
    1.17 +done
    1.18 +(*
    1.19 +apply (simp add: order_less_le abs_le_iff)  
    1.20  apply (auto simp add: abs_if minus_le_self_iff eq_minus_self_iff) 
    1.21 - apply (simp add:  linorder_not_less [symmetric]) 
    1.22 + apply (simp add:  linorder_not_less [symmetric])
    1.23  apply (simp add: le_minus_self_iff linorder_neq_iff) 
    1.24  apply (simp add:  linorder_not_less [symmetric]) 
    1.25  done
    1.26 +*)
    1.27  
    1.28  lemma abs_triangle_ineq: "abs (a+b) \<le> abs a + abs (b::'a::ordered_ring)"
    1.29  by (force simp add: abs_le_iff abs_ge_self abs_ge_minus_self add_mono)