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/WordBitwise.thy
changeset 57512 cc97b347b301
parent 55465 0d31c0546286
child 59058 a78612c67ec0 
--- a/src/HOL/Word/WordBitwise.thy	Fri Jul 04 20:07:08 2014 +0200
+++ b/src/HOL/Word/WordBitwise.thy	Fri Jul 04 20:18:47 2014 +0200
@@ -306,7 +306,7 @@
 
   show ?case
     using Cons
-    apply (simp add: trans [OF of_bl_append add_commute]
+    apply (simp add: trans [OF of_bl_append add.commute]
                      rbl_mul_simps rbl_word_plus'
                      Cons.hyps distrib_right mult_bit
                      shiftl rbl_shiftl)
isabelle