src/HOL/Algebra/FiniteProduct.thy
changeset 41090 b98fe4de1ecd
parent 40786 0a54cfc9add3
child 41433 1b8ff770f02c