src/HOL/Algebra/FiniteProduct.thy
changeset 23512 770e7f9f715b
parent 23350 50c5b0912a0c
child 23746 a455e69c31cc