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