src/HOL/Number_Theory/UniqueFactorization.thy
changeset 54381 9c1f21365326
parent 51548 757fa47af981
child 54611 31afce809794