src/HOL/NumberTheory/Factorization.thy
changeset 16480 abf475cf11f2
parent 16417 9bc16273c2d4
child 16663 13e9c402308b