src/HOL/Library/Float.thy

--- a/src/HOL/Library/Float.thy	Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Library/Float.thy	Mon Dec 07 10:38:04 2015 +0100
@@ -529,7 +529,7 @@
   show "m = mantissa f * 2 ^ nat (exponent f - e)" 
     by linarith
   show "e = exponent f - nat (exponent f - e)"
-    using `e \<le> exponent f` by auto
+    using \<open>e \<le> exponent f\<close> by auto
 qed
 
 context