src/HOL/Number_Theory/UniqueFactorization.thy
changeset 49821 d15fe10593ff
parent 49719 b2135b2730e8
child 49824 c26665a197dc