src/HOL/Number_Theory/UniqueFactorization.thy
changeset 60299 5ae2a2e74c93
parent 59010 ec2b4270a502
child 60495 d7ff0a1df90a