src/HOL/Algebra/FiniteProduct.thy
changeset 71035 6fe5a0e1fa8e
parent 70044 da5857dbcbb9