src/HOL/NumberTheory/Factorization.thy
changeset 24284 f5afd33f5d02
parent 23814 cdaa6b701509
child 24820 c0c7e6ebf35f