# HG changeset patch # User huffman # Date 1313849384 25200 # Node ID 49be3e7d4762309de729c41299e7ea68aee47e13 # Parent e5294bcf58a46f0390ac0b7f1f3e54d93844d9a3 remove some over-specific rules from the simpset diff -r e5294bcf58a4 -r 49be3e7d4762 src/HOL/RealDef.thy --- a/src/HOL/RealDef.thy Sat Aug 20 06:35:43 2011 -0700 +++ b/src/HOL/RealDef.thy Sat Aug 20 07:09:44 2011 -0700 @@ -1674,13 +1674,13 @@ lemma abs_le_interval_iff: "(abs x \ r) = (-r\x & x\(r::real))" by (force simp add: abs_le_iff) -lemma abs_add_one_gt_zero [simp]: "(0::real) < 1 + abs(x)" +lemma abs_add_one_gt_zero: "(0::real) < 1 + abs(x)" by (simp add: abs_if) lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)" by (rule abs_of_nonneg [OF real_of_nat_ge_zero]) -lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x" +lemma abs_add_one_not_less_self: "~ abs(x) + (1::real) < x" by simp lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \ abs(x + -l) + abs(y + -m)"