src/HOL/Algebra/FiniteProduct.thy
changeset 59009 348561aa3869
parent 58860 fee7cfa69c50
child 60112 3eab4acaa035