src/HOL/Algebra/FiniteProduct.thy
changeset 62098 b1b2834bb493
parent 61384 9f5145281888
child 62105 686681f69d5e