src/HOL/Library/Float.thy
changeset 60376 528a48f4ad87
parent 60017 b785d6d06430
child 60500 903bb1495239
     1.1 --- a/src/HOL/Library/Float.thy	Sun Jun 07 12:55:42 2015 +0200
     1.2 +++ b/src/HOL/Library/Float.thy	Sun Jun 07 14:36:36 2015 +0200
     1.3 @@ -1124,9 +1124,12 @@
     1.4  lift_definition rapprox_posrat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float"
     1.5    is "\<lambda>prec (x::nat) (y::nat). round_up (rat_precision prec x y) (x / y)" by simp
     1.6  
     1.7 -lemma compute_rapprox_posrat[code]:
     1.8 +context
     1.9 +  notes divmod_int_mod_div[simp]
    1.10 +begin
    1.11 +
    1.12 +qualified lemma compute_rapprox_posrat[code]:
    1.13    fixes prec x y
    1.14 -  notes divmod_int_mod_div[simp]
    1.15    defines "l \<equiv> rat_precision prec x y"
    1.16    shows "rapprox_posrat prec x y = (let
    1.17       l = l ;
    1.18 @@ -1163,7 +1166,8 @@
    1.19           (auto simp add: round_up_def ceil_divide_floor_conv floor_divide_eq_div [symmetric])
    1.20    qed
    1.21  qed
    1.22 -hide_fact (open) compute_rapprox_posrat
    1.23 +
    1.24 +end
    1.25  
    1.26  lemma rat_precision_pos:
    1.27    assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n"