Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Word/WordShift.thy
changeset 37654 8e33b9d04a82
parent 37604 1840dc0265da 
--- a/src/HOL/Word/WordShift.thy	Wed Jun 30 16:28:13 2010 +0200
+++ b/src/HOL/Word/WordShift.thy	Wed Jun 30 16:28:13 2010 +0200
@@ -13,7 +13,7 @@
 subsection "Bit shifting"
 
 lemma shiftl1_number [simp] :
-  "shiftl1 (number_of w) = number_of (w BIT bit.B0)"
+  "shiftl1 (number_of w) = number_of (w BIT 0)"
   apply (unfold shiftl1_def word_number_of_def)
   apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm
               del: BIT_simps)
@@ -27,7 +27,7 @@
 
 lemmas shiftl1_def_u = shiftl1_def [folded word_number_of_def]
 
-lemma shiftl1_def_s: "shiftl1 w = number_of (sint w BIT bit.B0)"
+lemma shiftl1_def_s: "shiftl1 w = number_of (sint w BIT 0)"
   by (rule trans [OF _ shiftl1_number]) simp
 
 lemma shiftr1_0 [simp] : "shiftr1 0 = 0"
isabelle