src/HOL/Algebra/FiniteProduct.thy
changeset 68300 cd8ab1a7a286
parent 67613 ce654b0e6d69
child 68445 c183a6a69f2d