src/HOL/Algebra/FiniteProduct.thy
changeset 67895 cd00999d2d30
parent 67613 ce654b0e6d69
child 68445 c183a6a69f2d