src/HOL/Algebra/FiniteProduct.thy
changeset 57978 8f4a332500e4
parent 56142 8bb21318e10b
child 58860 fee7cfa69c50