changeset 66453 | cc19f7ca2ed6 |
parent 66276 | acc3b7dd0b21 |
child 67108 | 6b350c594ae3 |
--- a/src/HOL/Number_Theory/Prime_Powers.thy Fri Aug 18 13:55:05 2017 +0200 +++ b/src/HOL/Number_Theory/Prime_Powers.thy Fri Aug 18 20:47:47 2017 +0200 @@ -6,7 +6,7 @@ *) section \<open>Prime powers\<close> theory Prime_Powers - imports Complex_Main "~~/src/HOL/Computational_Algebra/Primes" + imports Complex_Main "HOL-Computational_Algebra.Primes" begin definition aprimedivisor :: "'a :: normalization_semidom \<Rightarrow> 'a" where