remove some over-specific rules from the simpset
authorhuffman
Sat Aug 20 07:09:44 2011 -0700 (2011-08-20)
changeset 4434449be3e7d4762
parent 44343 e5294bcf58a4
child 44345 881c324470a2
remove some over-specific rules from the simpset
src/HOL/RealDef.thy
     1.1 --- a/src/HOL/RealDef.thy	Sat Aug 20 06:35:43 2011 -0700
     1.2 +++ b/src/HOL/RealDef.thy	Sat Aug 20 07:09:44 2011 -0700
     1.3 @@ -1674,13 +1674,13 @@
     1.4  lemma abs_le_interval_iff: "(abs x \<le> r) = (-r\<le>x & x\<le>(r::real))"
     1.5  by (force simp add: abs_le_iff)
     1.6  
     1.7 -lemma abs_add_one_gt_zero [simp]: "(0::real) < 1 + abs(x)"
     1.8 +lemma abs_add_one_gt_zero: "(0::real) < 1 + abs(x)"
     1.9  by (simp add: abs_if)
    1.10  
    1.11  lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)"
    1.12  by (rule abs_of_nonneg [OF real_of_nat_ge_zero])
    1.13  
    1.14 -lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x"
    1.15 +lemma abs_add_one_not_less_self: "~ abs(x) + (1::real) < x"
    1.16  by simp
    1.17   
    1.18  lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"