src/HOL/Number_Theory/UniqueFactorization.thy
changeset 36070 d80e5d3c8fe1
parent 35644 d20cf282342e
child 36903 489c1fbbb028