src/HOL/Number_Theory/UniqueFactorization.thy
changeset 39820 cd691e2c7a1a
parent 39302 d7728f65b353
child 40461 e876e95588ce