src/HOL/Ring_and_Field.thy
changeset 14398 c5c47703f763
parent 14387 e96d5c42c4b0
child 14421 ee97b6463cb4
--- a/src/HOL/Ring_and_Field.thy	Thu Feb 19 10:41:32 2004 +0100
+++ b/src/HOL/Ring_and_Field.thy	Thu Feb 19 15:57:34 2004 +0100
@@ -1526,6 +1526,7 @@
 by (simp add: abs_if linorder_neq_iff)
 
 lemma abs_not_less_zero [simp]: "~ abs a < (0::'a::ordered_ring)"
+apply (simp add: abs_if)
 by (simp add: abs_if  order_less_not_sym [of a 0])
 
 lemma abs_le_zero_iff [simp]: "(abs a \<le> (0::'a::ordered_ring)) = (a = 0)" 
@@ -1620,11 +1621,17 @@
 
 lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::ordered_ring))" 
 apply (simp add: order_less_le abs_le_iff)  
+apply (auto simp add: abs_if minus_le_self_iff eq_minus_self_iff)
+apply (simp add: le_minus_self_iff linorder_neq_iff) 
+done
+(*
+apply (simp add: order_less_le abs_le_iff)  
 apply (auto simp add: abs_if minus_le_self_iff eq_minus_self_iff) 
- apply (simp add:  linorder_not_less [symmetric]) 
+ apply (simp add:  linorder_not_less [symmetric])
 apply (simp add: le_minus_self_iff linorder_neq_iff) 
 apply (simp add:  linorder_not_less [symmetric]) 
 done
+*)
 
 lemma abs_triangle_ineq: "abs (a+b) \<le> abs a + abs (b::'a::ordered_ring)"
 by (force simp add: abs_le_iff abs_ge_self abs_ge_minus_self add_mono)