src/HOL/Number_Theory/UniqueFactorization.thy
changeset 55169 fda77499eef5
parent 55130 70db8d380d62
child 55242 413ec965f95d