# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1502986756 -7200
# Node ID 97ad7a583457f0e1bab89b2d0f1426d3757eaf7f
# Parent  a1f5c5c26fa676b2f7e8bb9f3def7f459830b9ec# Parent  aeb8b8fe94d0f6e6b04642bfb5de7c871bea666c
Merged

diff -r a1f5c5c26fa6 -r 97ad7a583457 src/HOL/Word/WordBitwise.thy
--- a/src/HOL/Word/WordBitwise.thy	Thu Aug 17 14:52:56 2017 +0200
+++ b/src/HOL/Word/WordBitwise.thy	Thu Aug 17 18:19:16 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: