src/HOL/Number_Theory/UniqueFactorization.thy
changeset 59366 e94df7f6b608
parent 59010 ec2b4270a502
child 60495 d7ff0a1df90a