src/HOL/Algebra/FiniteProduct.thy
changeset 82314 c95eca07f6a0
parent 81438 95c9af7483b1