diff -r f2e51e704a96 -r ab2e862263e7 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Int.thy	Mon Nov 02 11:56:28 2015 +0100
@@ -225,6 +225,9 @@
 lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
   by (transfer fixing: times) (clarsimp simp add: algebra_simps of_nat_mult)
 
+lemma mult_of_int_commute: "of_int x * y = y * of_int x"
+  by (transfer fixing: times) (auto simp: algebra_simps mult_of_nat_commute)
+
 text\<open>Collapse nested embeddings\<close>
 lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n"
 by (induct n) auto