src/HOL/Algebra/FiniteProduct.thy
changeset 28052 4dc09699cf93
parent 27933 4b867f6a65d3
child 28524 644b62cf678f