src/HOL/Algebra/FiniteProduct.thy
changeset 35272 c283ae736bea
parent 35054 a5db9779b026
child 35416 d8d7d1b785af