src/HOL/Real.thy

 apply (rule_tac x = " (min d1 d2) /2" in exI)
 apply (simp add: min_def)
 done
 
 
-text\<open>Similar results are proved in @{text Fields}\<close>
+text\<open>Similar results are proved in \<open>Fields\<close>\<close>
 lemma real_less_half_sum: "x < y ==> x < (x+y) / (2::real)"
   by auto
 
 lemma real_gt_half_sum: "x < y ==> (x+y)/(2::real) < y"
   by auto

     then have "i < b + j * b"
       by (metis linorder_not_less of_int_add of_int_le_iff of_int_mult order_trans_rules(21))
     moreover have "j * b < 1 + i"
     proof -
       have "real_of_int (j * b) < real_of_int i + 1"
-        using `a < 1 + real_of_int i` `real_of_int j * real_of_int b \<le> a` by force
+        using \<open>a < 1 + real_of_int i\<close> \<open>real_of_int j * real_of_int b \<le> a\<close> by force
       thus "j * b < 1 + i"
         by linarith
     qed
     ultimately have "(j - i div b) * b \<le> i mod b" "i mod b < ((j - i div b) + 1) * b"
       by (auto simp: field_simps)