src/HOL/Word/Bits_Int.thy

--- a/src/HOL/Word/Bits_Int.thy	Fri Jan 12 14:43:06 2018 +0100
+++ b/src/HOL/Word/Bits_Int.thy	Fri Jan 12 15:27:46 2018 +0100
@@ -609,7 +609,7 @@
     apply (auto simp: Bit_B0_2t [symmetric])
   done
 
-(*for use when simplifying with bin_nth_Bit*)
+\<comment> \<open>for use when simplifying with \<open>bin_nth_Bit\<close>\<close>
 lemma ex_eq_or: "(\<exists>m. n = Suc m \<and> (m = k \<or> P m)) \<longleftrightarrow> n = Suc k \<or> (\<exists>m. n = Suc m \<and> P m)"
   by auto