src/HOL/ex/Factorization.ML
changeset 9165 f46f407080f8
parent 8935 548901d05a0e
child 9747 043098ba5098