src/HOL/Old_Number_Theory/Factorization.thy
changeset 39359 6f49c7fbb1b1
parent 38159 e9b4835a54ee
child 41413 64cd30d6b0b8