src/HOL/Old_Number_Theory/Factorization.thy
changeset 38795 848be46708dc
parent 38159 e9b4835a54ee
child 41413 64cd30d6b0b8