--- a/src/HOL/Word/WordBitwise.thy Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Word/WordBitwise.thy Thu Aug 17 15:10:35 2017 +0200
@@ -34,7 +34,7 @@
text \<open>Breaking up word equalities into equalities on their
bit lists. Equalities are generated and manipulated in the
- reverse order to to_bl.\<close>
+ reverse order to @{const to_bl}.\<close>
lemma word_eq_rbl_eq: "x = y \<longleftrightarrow> rev (to_bl x) = rev (to_bl y)"
by simp
@@ -368,7 +368,7 @@
apply auto
done
-text \<open>Lemmas for unpacking rev (to_bl n) for numerals n and also
+text \<open>Lemmas for unpacking @{term "rev (to_bl n)"} for numerals n and also
for irreducible values and expressions.\<close>
lemma rev_bin_to_bl_simps: