src/HOL/Algebra/FiniteProduct.thy
changeset 57833 2c2bae3da1c2
parent 56142 8bb21318e10b
child 58860 fee7cfa69c50