src/HOL/Algebra/FiniteProduct.thy
changeset 60815 c93a83472eab
parent 60773 d09c66a0ea10
child 61382 efac889fccbc