src/HOL/NumberTheory/Factorization.thy
changeset 11401 26cbf43d76af
parent 11364 01020b10c0a7
child 11468 02cd5d5bc497