src/HOL/Algebra/FiniteProduct.thy
changeset 14470 1ffe42cfaefe
parent 14213 7bf882b0a51e
child 14590 276ef51cedbf