src/HOL/Number_Theory/UniqueFactorization.thy
changeset 33890 a87ad4be59a4
parent 33657 a4179bf442d1
child 34947 e1b8f2736404