src/HOL/Number_Theory/Residues.thy
changeset 66453 cc19f7ca2ed6
parent 66305 7454317f883c
child 66817 0b12755ccbb2
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Fri Aug 18 13:55:05 2017 +0200
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Fri Aug 18 20:47:47 2017 +0200
     1.3 @@ -10,10 +10,10 @@
     1.4  theory Residues
     1.5  imports
     1.6    Cong
     1.7 -  "~~/src/HOL/Algebra/More_Group"
     1.8 -  "~~/src/HOL/Algebra/More_Ring"
     1.9 -  "~~/src/HOL/Algebra/More_Finite_Product"
    1.10 -  "~~/src/HOL/Algebra/Multiplicative_Group"
    1.11 +  "HOL-Algebra.More_Group"
    1.12 +  "HOL-Algebra.More_Ring"
    1.13 +  "HOL-Algebra.More_Finite_Product"
    1.14 +  "HOL-Algebra.Multiplicative_Group"
    1.15    Totient
    1.16  begin
    1.17