src/HOL/Library/Float.thy
changeset 56479 91958d4b30f7
parent 56410 a14831ac3023
child 56536 aefb4a8da31f
     1.1 --- a/src/HOL/Library/Float.thy	Tue Apr 08 23:16:00 2014 +0200
     1.2 +++ b/src/HOL/Library/Float.thy	Wed Apr 09 09:37:47 2014 +0200
     1.3 @@ -637,7 +637,7 @@
     1.4    qed
     1.5    thus ?thesis using `\<not> b dvd a` by simp
     1.6  qed (simp add: ceiling_def real_of_int_minus[symmetric] divide_minus_left[symmetric]
     1.7 -               floor_divide_eq_div dvd_neg_div del: real_of_int_minus)
     1.8 +  floor_divide_eq_div dvd_neg_div del: divide_minus_left real_of_int_minus)
     1.9  
    1.10  lemma compute_float_up[code]:
    1.11    "float_up p (Float m e) =
    1.12 @@ -1004,7 +1004,7 @@
    1.13        else (if 0 < y
    1.14          then - (rapprox_posrat prec (nat (-x)) (nat y))
    1.15          else lapprox_posrat prec (nat (-x)) (nat (-y))))"
    1.16 -  by transfer (auto simp: round_up_def divide_minus_left divide_minus_right round_down_def ceiling_def ac_simps)
    1.17 +  by transfer (auto simp: round_up_def round_down_def ceiling_def ac_simps)
    1.18  hide_fact (open) compute_lapprox_rat
    1.19  
    1.20  lift_definition rapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" is
    1.21 @@ -1019,7 +1019,7 @@
    1.22        else (if 0 < y
    1.23          then - (lapprox_posrat prec (nat (-x)) (nat y))
    1.24          else rapprox_posrat prec (nat (-x)) (nat (-y))))"
    1.25 -  by transfer (auto simp: round_up_def round_down_def divide_minus_left divide_minus_right ceiling_def ac_simps)
    1.26 +  by transfer (auto simp: round_up_def round_down_def ceiling_def ac_simps)
    1.27  hide_fact (open) compute_rapprox_rat
    1.28  
    1.29  subsection {* Division *}