src/HOL/Number_Theory/UniqueFactorization.thy
changeset 51085 d90218288d51
parent 50027 7747a9f4c358
child 51489 f738e6dbd844