src/HOL/Old_Number_Theory/Factorization.thy
changeset 40744 0e7c2957fc1d
parent 38159 e9b4835a54ee
child 41413 64cd30d6b0b8