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