src/HOL/Algebra/Exponent.thy

--- a/src/HOL/Algebra/Exponent.thy	Thu Apr 06 08:33:37 2017 +0200
+++ b/src/HOL/Algebra/Exponent.thy	Thu Apr 06 21:37:13 2017 +0200
@@ -6,7 +6,7 @@
 *)
 
 theory Exponent
-imports Main "~~/src/HOL/Number_Theory/Primes"
+imports Main "~~/src/HOL/Computational_Algebra/Primes"
 begin
 
 section \<open>Sylow's Theorem\<close>