diff -r 1a20fd9cf281 -r eb4ddd18d635 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Sun Apr 24 21:31:14 2016 +0200
+++ b/src/HOL/Library/Float.thy	Mon Apr 25 16:09:26 2016 +0200
@@ -953,7 +953,7 @@
       then show ?thesis by simp
     next
       case False
-      def n \<equiv> "\<lfloor>log 2 (real_of_int x)\<rfloor>"
+      define n where "n = \<lfloor>log 2 (real_of_int x)\<rfloor>"
       then have "0 \<le> n"
         using \<open>2 \<le> x\<close> by simp
       from \<open>2 \<le> x\<close> False have "x mod 2 = 1" "\<not> 2 dvd x"
@@ -1306,7 +1306,7 @@
   show ?thesis
   proof (cases "0 \<le> l")
     case True
-    def x' \<equiv> "x * 2 ^ nat l"
+    define x' where "x' = x * 2 ^ nat l"
     have "int x * 2 ^ nat l = x'"
       by (simp add: x'_def of_nat_mult of_nat_power)
     moreover have "real x * 2 powr l = real x'"
@@ -1319,7 +1319,7 @@
       by (metis floor_divide_of_int_eq of_int_of_nat_eq)
    next
     case False
-    def y' \<equiv> "y * 2 ^ nat (- l)"
+    define y' where "y' = 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 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'"
@@ -1683,14 +1683,14 @@
   then show ?thesis by simp
 next
   case False
-  def k \<equiv> "\<lfloor>log 2 \<bar>ai\<bar>\<rfloor>"
+  define k where "k = \<lfloor>log 2 \<bar>ai\<bar>\<rfloor>"
   then have "\<lfloor>log 2 \<bar>ai\<bar>\<rfloor> = k"
     by simp
   then have k: "2 powr k \<le> \<bar>ai\<bar>" "\<bar>ai\<bar> < 2 powr (k + 1)"
     by (simp_all add: floor_log_eq_powr_iff \<open>ai \<noteq> 0\<close>)
   have "k \<ge> 0"
     using assms by (auto simp: k_def)
-  def r \<equiv> "\<bar>ai\<bar> - 2 ^ nat k"
+  define r where "r = \<bar>ai\<bar> - 2 ^ nat k"
   have r: "0 \<le> r" "r < 2 powr k"
     using \<open>k \<ge> 0\<close> k
     by (auto simp: r_def k_def algebra_simps powr_add abs_if powr_int)