src/HOL/ex/Factorization.ML
changeset 9369 139fde7af7bd
parent 8935 548901d05a0e
child 9747 043098ba5098