equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 section \<open>The Nonstandard Primes as an Extension of the Prime Numbers\<close> |
7 section \<open>The Nonstandard Primes as an Extension of the Prime Numbers\<close> |
8 |
8 |
9 theory NSPrimes |
9 theory NSPrimes |
10 imports "~~/src/HOL/Computational_Algebra/Primes" "../Hyperreal" |
10 imports "HOL-Computational_Algebra.Primes" "HOL-Nonstandard_Analysis.Hyperreal" |
11 begin |
11 begin |
12 |
12 |
13 text \<open>These can be used to derive an alternative proof of the infinitude of |
13 text \<open>These can be used to derive an alternative proof of the infinitude of |
14 primes by considering a property of nonstandard sets.\<close> |
14 primes by considering a property of nonstandard sets.\<close> |
15 |
15 |