src/HOL/Number_Theory/UniqueFactorization.thy
changeset 39560 c13b4589fddf
parent 39302 d7728f65b353
child 40461 e876e95588ce