src/HOL/Old_Number_Theory/WilsonRuss.thy
changeset 44821 a92f65e174cf
parent 44766 d4d33a4d7548
child 47163 248376f8881d
     1.1 --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Wed Sep 07 14:58:40 2011 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Wed Sep 07 09:02:58 2011 -0700
     1.3 @@ -122,7 +122,7 @@
     1.4  lemma inv_inv_aux: "5 \<le> p ==>
     1.5      nat (p - 2) * nat (p - 2) = Suc (nat (p - 1) * nat (p - 3))"
     1.6    apply (subst int_int_eq [symmetric])
     1.7 -  apply (simp add: zmult_int [symmetric])
     1.8 +  apply (simp add: of_nat_mult)
     1.9    apply (simp add: left_diff_distrib right_diff_distrib)
    1.10    done
    1.11