src/HOL/Algebra/FiniteProduct.thy
changeset 80613 42408be39d6c
parent 70044 da5857dbcbb9