src/HOL/Algebra/FiniteProduct.thy
changeset 35721 f7bbee848403
parent 35416 d8d7d1b785af
child 35847 19f1f7066917