src/HOL/Real/RealDef.thy
changeset 16888 7cb4bcfa058e
parent 16819 00d8f9300d13
child 16973 b2a894562b8f
     1.1 --- a/src/HOL/Real/RealDef.thy	Tue Jul 19 17:21:59 2005 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Tue Jul 19 17:24:09 2005 +0200
     1.3 @@ -701,6 +701,9 @@
     1.4  lemma real_of_int_le_zero_cancel_iff [simp]: "(real (n::int) <= 0) = (n <= 0)"
     1.5  by (simp add: real_of_int_def)
     1.6  
     1.7 +lemma real_of_int_abs [simp]: "real (abs x) = abs(real (x::int))"
     1.8 +by (auto simp add: abs_if)
     1.9 +
    1.10  lemma int_less_real_le: "((n::int) < m) = (real n + 1 <= real m)"
    1.11    apply (subgoal_tac "real n + 1 = real (n + 1)")
    1.12    apply (simp del: real_of_int_add)