src/HOL/Number_Theory/UniqueFactorization.thy
changeset 36377 b3dce4c715d0
parent 35644 d20cf282342e
child 36903 489c1fbbb028