fix document
authorLars Hupel <lars.hupel@mytum.de>
Thu, 17 Aug 2017 15:10:35 +0200
changeset 66447 aeb8b8fe94d0
parent 66445 407de0768126
child 66448 97ad7a583457
fix document
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: