src/HOL/NumberTheory/Factorization.thy
changeset 11295 66925f23ac7f
parent 11049 7eef34adb852
child 11364 01020b10c0a7