src/HOL/Real/RealDef.thy
changeset 15003 6145dd7538d7
parent 14754 a080eeeaec14
child 15013 34264f5e4691
--- a/src/HOL/Real/RealDef.thy	Thu Jun 24 17:51:28 2004 +0200
+++ b/src/HOL/Real/RealDef.thy	Thu Jun 24 17:52:02 2004 +0200
@@ -830,16 +830,16 @@
 
 text{*FIXME: these should go!*}
 lemma abs_eqI1: "(0::real)\<le>x ==> abs x = x"
-by (simp add: real_abs_def)
+by (simp add: abs_if)
 
 lemma abs_eqI2: "(0::real) < x ==> abs x = x"
-by (simp add: real_abs_def)
+by (simp add: abs_if)
 
 lemma abs_minus_eqI2: "x < (0::real) ==> abs x = -x"
-by (simp add: real_abs_def linorder_not_less [symmetric])
+by (simp add: abs_if linorder_not_less [symmetric])
 
 lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))"
-by (simp add: real_abs_def)
+by (simp add: abs_if)
 
 lemma abs_interval_iff: "(abs x < r) = (-r < x & x < (r::real))"
 by (force simp add: Ring_and_Field.abs_less_iff)
@@ -849,7 +849,7 @@
 
 (*FIXME: used only once, in SEQ.ML*)
 lemma abs_add_one_gt_zero [simp]: "(0::real) < 1 + abs(x)"
-by (simp add: real_abs_def)
+by (simp add: abs_if)
 
 lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)"
 by (auto intro: abs_eqI1 simp add: real_of_nat_ge_zero)