src/HOL/NumberTheory/Factorization.thy
changeset 10618 5b96bc5fbec3
parent 9944 2a705d1af4dc
child 11049 7eef34adb852