equal
deleted
inserted
replaced
4 Copyright 2000 University of Cambridge |
4 Copyright 2000 University of Cambridge |
5 *) |
5 *) |
6 |
6 |
7 header {* Fundamental Theorem of Arithmetic (unique factorization into primes) *} |
7 header {* Fundamental Theorem of Arithmetic (unique factorization into primes) *} |
8 |
8 |
9 theory Factorization imports Primes Permutation begin |
9 theory Factorization |
|
10 imports Main Primes Permutation |
|
11 begin |
10 |
12 |
11 |
13 |
12 subsection {* Definitions *} |
14 subsection {* Definitions *} |
13 |
15 |
14 definition |
16 definition |