src/HOL/Algebra/FiniteProduct.thy
changeset 16129 6fa9ace50240
parent 15328 35951e6a7855
child 16417 9bc16273c2d4