src/HOL/NumberTheory/Factorization.thy
changeset 26113 ba5909699cc3
parent 25687 f92c9dfa7681
child 26316 9e9e67e33557