src/HOL/Algebra/FiniteProduct.thy
changeset 14360 e654599b114e
parent 14213 7bf882b0a51e
child 14590 276ef51cedbf