src/HOL/Algebra/FiniteProduct.thy
changeset 31991 37390299214a
parent 31727 2621a957d417
child 32693 6c6b1ba5e71e