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/Word_Miscellaneous.thy
changeset 57514 bdc2c6b40bf2
parent 57512 cc97b347b301
child 58681 a478a0742a8e 
--- a/src/HOL/Word/Word_Miscellaneous.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Word/Word_Miscellaneous.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -331,7 +331,7 @@
    prefer 2
    apply (erule asm_rl)
   apply (rule_tac f="%n. n div f" in arg_cong)
-  apply (simp add : mult_ac)
+  apply (simp add : ac_simps)
   done
     
 lemma diff_mod_le: "(a::nat) < d ==> b dvd d ==> a - a mod b <= d - b"
isabelle