src/HOL/Old_Number_Theory/Factorization.thy
changeset 61898 6c7861f783fd
parent 61382 efac889fccbc
child 62481 b5d8e57826df