src/HOL/Algebra/FiniteProduct.thy
changeset 20192 956cd30ef3be
parent 16638 3dc904d93767
child 20318 0e0ea63fe768