src/HOL/Algebra/FiniteProduct.thy
changeset 33085 c1b6cc29496b
parent 32960 69916a850301
child 35054 a5db9779b026