src/HOL/Algebra/FiniteProduct.thy
changeset 37724 6607ccf77946
parent 35849 b5522b51cb1e
child 40786 0a54cfc9add3