src/HOL/Nat.thy
changeset 61649 268d88ec9087
parent 61531 ab2e862263e7
child 61799 4cf66f21b764
     1.1 --- a/src/HOL/Nat.thy	Thu Nov 12 11:22:26 2015 +0100
     1.2 +++ b/src/HOL/Nat.thy	Fri Nov 13 12:27:13 2015 +0000
     1.3 @@ -1469,7 +1469,7 @@
     1.4  lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
     1.5    by (induct m) (simp_all add: ac_simps)
     1.6  
     1.7 -lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"
     1.8 +lemma of_nat_mult [simp]: "of_nat (m * n) = of_nat m * of_nat n"
     1.9    by (induct m) (simp_all add: ac_simps distrib_right)
    1.10  
    1.11  lemma mult_of_nat_commute: "of_nat x * y = y * of_nat x"