src/HOL/Number_Theory/UniqueFactorization.thy
changeset 39905 0bfaaa81fc62
parent 39302 d7728f65b353
child 40461 e876e95588ce