src/HOL/ex/Factorization.thy
changeset 9436 62bb04ab4b01
parent 8353 57a163920480