src/HOL/Algebra/FiniteProduct.thy
changeset 61068 6cb92c2a5ece
parent 60773 d09c66a0ea10
child 61382 efac889fccbc