src/HOL/Library/Float.thy

   show ?thesis
   proof (cases "0 \<le> l")
     case True
     def x' \<equiv> "x * 2 ^ nat l"
     have "int x * 2 ^ nat l = x'"
-      by (simp add: x'_def int_mult of_nat_power)
+      by (simp add: x'_def of_nat_mult of_nat_power)
     moreover have "real x * 2 powr l = real x'"
       by (simp add: powr_realpow[symmetric] \<open>0 \<le> l\<close> x'_def)
     ultimately show ?thesis
       using ceil_divide_floor_conv[of y x'] powr_realpow[of 2 "nat l"] \<open>0 \<le> l\<close> \<open>y \<noteq> 0\<close>
         l_def[symmetric, THEN meta_eq_to_obj_eq]

       by (metis floor_divide_of_int_eq of_int_of_nat_eq)
    next
     case False
     def y' \<equiv> "y * 2 ^ nat (- l)"
     from \<open>y \<noteq> 0\<close> have "y' \<noteq> 0" by (simp add: y'_def)
-    have "int y * 2 ^ nat (- l) = y'" by (simp add: y'_def int_mult of_nat_power)
+    have "int y * 2 ^ nat (- l) = y'" by (simp add: y'_def of_nat_mult of_nat_power)
     moreover have "real x * real_of_int (2::int) powr real_of_int l / real y = x / real y'"
       using \<open>\<not> 0 \<le> l\<close>
       by (simp add: powr_realpow[symmetric] powr_minus y'_def field_simps)
     ultimately show ?thesis
       using ceil_divide_floor_conv[of y' x] \<open>\<not> 0 \<le> l\<close> \<open>y' \<noteq> 0\<close> \<open>y \<noteq> 0\<close>