src/HOL/Algebra/FiniteProduct.thy
changeset 59555 05573e5504a9
parent 58860 fee7cfa69c50
child 60112 3eab4acaa035