src/HOL/Old_Number_Theory/Factorization.thy
changeset 58013 14c8269d0de9
parent 57983 6edc3529bb4e
child 58889 5b7a9633cfa8