--- a/src/HOL/Complex/ex/NSPrimes.thy Thu Aug 19 10:33:10 2004 +0200
+++ b/src/HOL/Complex/ex/NSPrimes.thy Thu Aug 19 12:35:45 2004 +0200
@@ -6,7 +6,9 @@
header{*The Nonstandard Primes as an Extension of the Prime Numbers*}
-theory NSPrimes = "~~/src/HOL/NumberTheory/Factorization" + Complex_Main:
+theory NSPrimes
+imports "~~/src/HOL/NumberTheory/Factorization" Complex_Main
+begin
text{*These can be used to derive an alternative proof of the infinitude of
primes by considering a property of nonstandard sets.*}