src/HOL/Algebra/FiniteProduct.thy
changeset 37928 24785fa2416c
parent 35849 b5522b51cb1e
child 40786 0a54cfc9add3