equal
deleted
inserted
replaced
2 Author : Jacques D. Fleuriot |
2 Author : Jacques D. Fleuriot |
3 Copyright : 2002 University of Edinburgh |
3 Copyright : 2002 University of Edinburgh |
4 Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
4 Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
5 *) |
5 *) |
6 |
6 |
7 header{*The Nonstandard Primes as an Extension of the Prime Numbers*} |
7 section{*The Nonstandard Primes as an Extension of the Prime Numbers*} |
8 |
8 |
9 theory NSPrimes |
9 theory NSPrimes |
10 imports "~~/src/HOL/Number_Theory/UniqueFactorization" "../Hyperreal" |
10 imports "~~/src/HOL/Number_Theory/UniqueFactorization" "../Hyperreal" |
11 begin |
11 begin |
12 |
12 |