src/HOL/Number_Theory/UniqueFactorization.thy
changeset 49063 f93443defa6c
parent 48822 21d4ed91912f
child 49716 c55b39740529