src/HOL/Algebra/FiniteProduct.thy
changeset 62627 20288ba55e85
parent 62105 686681f69d5e
child 63167 0909deb8059b