src/HOL/Algebra/FiniteProduct.thy
changeset 40407 2ff10e613689
parent 35849 b5522b51cb1e
child 40786 0a54cfc9add3