src/HOL/Number_Theory/UniqueFactorization.thy
changeset 36832 e6078ef937df
parent 35644 d20cf282342e
child 36903 489c1fbbb028