src/HOL/Algebra/FiniteProduct.thy
changeset 63132 8230358fab88
parent 62105 686681f69d5e
child 63167 0909deb8059b