src/HOL/Number_Theory/UniqueFactorization.thy
changeset 60634 e3b6e516608b
parent 60567 19c277ea65ae
child 60981 e1159bd15982