# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1502975435 -7200
# Node ID aeb8b8fe94d0f6e6b04642bfb5de7c871bea666c
# Parent  407de076812651abf429562f3bbf8e434927d64c
fix document

diff -r 407de0768126 -r aeb8b8fe94d0 src/HOL/Word/WordBitwise.thy
--- 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: