src/HOL/Number_Theory/UniqueFactorization.thy
changeset 55719 cdddd073bff8
parent 55242 413ec965f95d
child 57418 6ab1c7cb0b8d