src/HOL/Number_Theory/Cong.thy
changeset 65417 fc41a5650fb1
parent 64593 50c715579715
child 66380 96ff0eb8294a
--- a/src/HOL/Number_Theory/Cong.thy	Thu Apr 06 08:33:37 2017 +0200
+++ b/src/HOL/Number_Theory/Cong.thy	Thu Apr 06 21:37:13 2017 +0200
@@ -26,7 +26,7 @@
 section \<open>Congruence\<close>
 
 theory Cong
-imports Primes
+imports "~~/src/HOL/Computational_Algebra/Primes"
 begin
 
 subsection \<open>Turn off \<open>One_nat_def\<close>\<close>