src/HOL/Real/RealDef.thy
changeset 20217 25b068a99d2b
parent 19765 dfe940911617
child 20485 3078fd2eec7b
     1.1 --- a/src/HOL/Real/RealDef.thy	Wed Jul 26 13:31:07 2006 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Wed Jul 26 19:23:04 2006 +0200
     1.3 @@ -1024,15 +1024,9 @@
     1.4  by (simp add: real_of_nat_ge_zero)
     1.5  
     1.6  lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x"
     1.7 -apply (simp add: linorder_not_less)
     1.8 -apply (auto intro: abs_ge_self [THEN order_trans])
     1.9 -done
    1.10 +by simp
    1.11   
    1.12  lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
    1.13 -apply (simp add: real_add_assoc)
    1.14 -apply (rule_tac a1 = y in add_left_commute [THEN ssubst])
    1.15 -apply (rule real_add_assoc [THEN subst])
    1.16 -apply (rule abs_triangle_ineq)
    1.17 -done
    1.18 +by simp
    1.19  
    1.20  end