src/HOL/Algebra/FiniteProduct.thy
changeset 37693 b10444eb9c98
parent 35849 b5522b51cb1e
child 40786 0a54cfc9add3