src/HOL/Nat.thy

   by (simp add: of_nat_def)
 
 lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
   by (induct m) (simp_all add: ac_simps)
 
-lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"
+lemma of_nat_mult [simp]: "of_nat (m * n) = of_nat m * of_nat n"
   by (induct m) (simp_all add: ac_simps distrib_right)
 
 lemma mult_of_nat_commute: "of_nat x * y = y * of_nat x"
   by (induction x) (simp_all add: algebra_simps)