src/HOL/Number_Theory/UniqueFactorization.thy
changeset 60634 e3b6e516608b
parent 60567 19c277ea65ae
child 60981 e1159bd15982
equal deleted inserted replaced
60633:f758c40e0a9a 60634:e3b6e516608b