src/HOL/Number_Theory/Residues.thy
changeset 68447 0beb927eed89
parent 67341 df79ef3b3a41
child 68458 023b353911c5
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Thu Jun 14 14:23:48 2018 +0100
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Thu Jun 14 15:20:10 2018 +0100
     1.3 @@ -10,9 +10,6 @@
     1.4  theory Residues
     1.5  imports
     1.6    Cong
     1.7 -  "HOL-Algebra.More_Group"
     1.8 -  "HOL-Algebra.More_Ring"
     1.9 -  "HOL-Algebra.More_Finite_Product"
    1.10    "HOL-Algebra.Multiplicative_Group"
    1.11    Totient
    1.12  begin
    1.13 @@ -355,7 +352,7 @@
    1.14       apply (metis Units_inv_inv)+
    1.15      done
    1.16    also have "\<dots> = \<one>"
    1.17 -    apply (rule finprod_one)
    1.18 +    apply (rule finprod_one_eqI)
    1.19       apply auto
    1.20      apply (subst finprod_insert)
    1.21          apply auto