src/HOL/Number_Theory/UniqueFactorization.thy
changeset 57822 9ea92df3631a
parent 57418 6ab1c7cb0b8d
child 58889 5b7a9633cfa8