src/HOL/Algebra/FiniteProduct.thy
changeset 28387 f77f54f55319
parent 27933 4b867f6a65d3
child 28524 644b62cf678f