src/HOL/Number_Theory/UniqueFactorization.thy
changeset 50739 5165d7e6d3b9
parent 50027 7747a9f4c358
child 51489 f738e6dbd844