src/HOL/NewNumberTheory/UniqueFactorization.thy
changeset 32478 87201c60ae7d
parent 31952 40501bb2d57c