src/HOL/Number_Theory/UniqueFactorization.thy
changeset 61095 50e793295ce1
parent 60981 e1159bd15982
child 61714 7c1ad030f0c9