src/HOL/Algebra/FiniteProduct.thy
changeset 14024 213dcc39358f
parent 13936 d3671b878828
child 14213 7bf882b0a51e