src/HOL/Old_Number_Theory/Factorization.thy
changeset 39368 f661064b2b80
parent 38159 e9b4835a54ee
child 41413 64cd30d6b0b8