src/HOL/Library/Float.thy
changeset 58834 773b378d9313
parent 58410 6d46ad54a2ab
child 58881 b9556a055632
     1.1 --- a/src/HOL/Library/Float.thy	Thu Oct 30 16:36:44 2014 +0000
     1.2 +++ b/src/HOL/Library/Float.thy	Thu Oct 30 21:02:01 2014 +0100
     1.3 @@ -935,8 +935,7 @@
     1.4        unfolding normfloat_def
     1.5        using ceil_divide_floor_conv[of y x'] powr_realpow[of 2 "nat l"] `0 \<le> l` `y \<noteq> 0`
     1.6          l_def[symmetric, THEN meta_eq_to_obj_eq]
     1.7 -      by transfer
     1.8 -         (simp add: floor_divide_eq_div[symmetric] dvd_eq_mod_eq_0 round_up_def)
     1.9 +      by transfer (auto simp add: floor_divide_eq_div [symmetric] round_up_def)
    1.10     next
    1.11      assume "\<not> 0 \<le> l"
    1.12      def y' \<equiv> "y * 2 ^ nat (- l)"
    1.13 @@ -950,7 +949,7 @@
    1.14        using ceil_divide_floor_conv[of y' x] `\<not> 0 \<le> l` `y' \<noteq> 0` `y \<noteq> 0`
    1.15          l_def[symmetric, THEN meta_eq_to_obj_eq]
    1.16        by transfer
    1.17 -         (simp add: round_up_def ceil_divide_floor_conv floor_divide_eq_div[symmetric] dvd_eq_mod_eq_0)
    1.18 +         (auto simp add: round_up_def ceil_divide_floor_conv floor_divide_eq_div [symmetric])
    1.19    qed
    1.20  qed
    1.21  hide_fact (open) compute_rapprox_posrat