src/HOL/Algebra/FiniteProduct.thy
changeset 29457 2eadbc24de8c
parent 29237 e90d9d51106b
child 31727 2621a957d417