src/HOL/Algebra/FiniteProduct.thy
changeset 62337 d3996d5873dd
parent 62105 686681f69d5e
child 63167 0909deb8059b