--- 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