src/HOL/Algebra/FiniteProduct.thy
changeset 31760 05e3e5980677
parent 31727 2621a957d417
child 32693 6c6b1ba5e71e