src/HOL/Proofs/Extraction/Euclid.thy
changeset 65417 fc41a5650fb1
parent 63830 2ea3725a34bd
child 66258 2b83dd24b301
--- a/src/HOL/Proofs/Extraction/Euclid.thy	Thu Apr 06 08:33:37 2017 +0200
+++ b/src/HOL/Proofs/Extraction/Euclid.thy	Thu Apr 06 21:37:13 2017 +0200
@@ -8,7 +8,7 @@
 
 theory Euclid
 imports
-  "~~/src/HOL/Number_Theory/Primes"
+  "~~/src/HOL/Computational_Algebra/Primes"
   Util
   "~~/src/HOL/Library/Code_Target_Numeral"
 begin