src/HOL/Old_Number_Theory/Factorization.thy
changeset 64274 c8990e5feac9
parent 62481 b5d8e57826df