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/Library/Code_Target_Int.thy
changeset 64242 93c6f0da5c70
parent 63351 e5d08b1d8fea
child 64997 067a6cca39f0 
--- a/src/HOL/Library/Code_Target_Int.thy	Sun Oct 16 09:31:04 2016 +0200
+++ b/src/HOL/Library/Code_Target_Int.thy	Sun Oct 16 09:31:05 2016 +0200
@@ -115,7 +115,7 @@
        j = k mod 2
      in if j = 0 then l else l + 1)"
 proof -
-  from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
+  from div_mult_mod_eq have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
   show ?thesis
     by (simp add: Let_def of_int_add [symmetric]) (simp add: * mult.commute)
 qed
isabelle