src/HOL/Number_Theory/UniqueFactorization.thy
changeset 60057 86fa63ce8156
parent 59010 ec2b4270a502
child 60495 d7ff0a1df90a