src/HOL/ex/Factorization.ML
changeset 9771 54c6a2c6e569
parent 9747 043098ba5098
child 9826 5b5d9ee742ca