src/HOL/Number_Theory/Prime_Powers.thy
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