--- a/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy Thu Apr 06 08:33:37 2017 +0200
+++ b/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy Thu Apr 06 21:37:13 2017 +0200
@@ -7,7 +7,7 @@
section \<open>The Nonstandard Primes as an Extension of the Prime Numbers\<close>
theory NSPrimes
- imports "~~/src/HOL/Number_Theory/Primes" "../Hyperreal"
+ imports "~~/src/HOL/Computational_Algebra/Primes" "../Hyperreal"
begin
text \<open>These can be used to derive an alternative proof of the infinitude of