src/HOL/Algebra/FiniteProduct.thy
changeset 82704 e0fb46018187
parent 81438 95c9af7483b1