src/HOL/Library/Float.thy
 changeset 56410 a14831ac3023 parent 55945 e96383acecf9 child 56479 91958d4b30f7
```     1.1 --- a/src/HOL/Library/Float.thy	Thu Apr 03 23:51:52 2014 +0100
1.2 +++ b/src/HOL/Library/Float.thy	Fri Apr 04 17:58:25 2014 +0100
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: divide_minus_left real_of_int_minus)
1.8 +               floor_divide_eq_div dvd_neg_div del: 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 round_down_def ceiling_def ac_simps)
1.17 +  by transfer (auto simp: round_up_def divide_minus_left divide_minus_right 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 ceiling_def ac_simps)
1.26 +  by transfer (auto simp: round_up_def round_down_def divide_minus_left divide_minus_right ceiling_def ac_simps)
1.27  hide_fact (open) compute_rapprox_rat
1.28
1.29  subsection {* Division *}
```