src/HOL/Number_Theory/UniqueFactorization.thy
changeset 61766 507b39df1a57
parent 61714 7c1ad030f0c9
child 61762 d50b993b4fb9