src/HOL/Number_Theory/UniqueFactorization.thy
changeset 33890 a87ad4be59a4
parent 33657 a4179bf442d1
child 34947 e1b8f2736404
equal deleted inserted replaced
33889:4328de748fb2 33890:a87ad4be59a4