src/HOL/Number_Theory/UniqueFactorization.thy
changeset 33155 78c10ce27f09
parent 32479 521cc9bf2958
child 33657 a4179bf442d1