src/HOL/Algebra/FiniteProduct.thy
changeset 61095 50e793295ce1
parent 60773 d09c66a0ea10
child 61382 efac889fccbc