src/HOL/Algebra/FiniteProduct.thy
changeset 31762 20745ab5b79a
parent 31727 2621a957d417
child 32693 6c6b1ba5e71e