src/HOL/Algebra/FiniteProduct.thy
changeset 67405 e9ab4ad7bd15
parent 67341 df79ef3b3a41
child 67613 ce654b0e6d69