src/HOL/Number_Theory/UniqueFactorization.thy
changeset 33003 1c93cfa807bc
parent 32479 521cc9bf2958
child 33657 a4179bf442d1