changeset 27368 | 9f90ac19e32b |
parent 26316 | 9e9e67e33557 |
--- a/src/HOL/NumberTheory/Factorization.thy Thu Jun 26 10:06:54 2008 +0200 +++ b/src/HOL/NumberTheory/Factorization.thy Thu Jun 26 10:07:01 2008 +0200 @@ -6,7 +6,9 @@ header {* Fundamental Theorem of Arithmetic (unique factorization into primes) *} -theory Factorization imports Primes Permutation begin +theory Factorization +imports Main Primes Permutation +begin subsection {* Definitions *}