src/HOL/Algebra/FiniteProduct.thy
changeset 54257 5c7a3b6b05a9
parent 46721 f88b187ad8ca
child 56142 8bb21318e10b