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 *}
```