src/HOL/Number_Theory/UniqueFactorization.thy
changeset 40681 872b08416fb4
parent 40461 e876e95588ce
child 41413 64cd30d6b0b8