| changeset 16417 | 9bc16273c2d4 |
| parent 15229 | 1eb23f805c06 |
| child 16663 | 13e9c402308b |
--- a/src/HOL/NumberTheory/IntPrimes.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/NumberTheory/IntPrimes.thy Fri Jun 17 16:12:49 2005 +0200 @@ -11,7 +11,7 @@ header {* Divisibility and prime numbers (on integers) *} -theory IntPrimes = Primes: +theory IntPrimes imports Primes begin text {* The @{text dvd} relation, GCD, Euclid's extended algorithm, primes,