changeset 66453 | cc19f7ca2ed6 |
parent 66305 | 7454317f883c |
child 66817 | 0b12755ccbb2 |
--- a/src/HOL/Number_Theory/Residues.thy Fri Aug 18 13:55:05 2017 +0200 +++ b/src/HOL/Number_Theory/Residues.thy Fri Aug 18 20:47:47 2017 +0200 @@ -10,10 +10,10 @@ theory Residues imports Cong - "~~/src/HOL/Algebra/More_Group" - "~~/src/HOL/Algebra/More_Ring" - "~~/src/HOL/Algebra/More_Finite_Product" - "~~/src/HOL/Algebra/Multiplicative_Group" + "HOL-Algebra.More_Group" + "HOL-Algebra.More_Ring" + "HOL-Algebra.More_Finite_Product" + "HOL-Algebra.Multiplicative_Group" Totient begin