# HG changeset patch
# User wenzelm
# Date 1433680596 -7200
# Node ID 528a48f4ad87a13fcfe1b7530c0189a81ec7bbfc
# Parent  b35b08a143b2c0716c9490d5e39d16fa068bb27d
tuned;

diff -r b35b08a143b2 -r 528a48f4ad87 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Sun Jun 07 12:55:42 2015 +0200
+++ b/src/HOL/Library/Float.thy	Sun Jun 07 14:36:36 2015 +0200
@@ -1124,9 +1124,12 @@
 lift_definition rapprox_posrat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float"
   is "\<lambda>prec (x::nat) (y::nat). round_up (rat_precision prec x y) (x / y)" by simp
 
-lemma compute_rapprox_posrat[code]:
+context
+  notes divmod_int_mod_div[simp]
+begin
+
+qualified lemma compute_rapprox_posrat[code]:
   fixes prec x y
-  notes divmod_int_mod_div[simp]
   defines "l \<equiv> rat_precision prec x y"
   shows "rapprox_posrat prec x y = (let
      l = l ;
@@ -1163,7 +1166,8 @@
          (auto simp add: round_up_def ceil_divide_floor_conv floor_divide_eq_div [symmetric])
   qed
 qed
-hide_fact (open) compute_rapprox_posrat
+
+end
 
 lemma rat_precision_pos:
   assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n"