# 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 \<le> r) = (-r\<le>x & x\<le>(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)) \<le> abs(x + -l) + abs(y + -m)"