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>