src/HOL/Algebra/FiniteProduct.thy
changeset 69133 22fe10b4c0c6
parent 68517 6b5f15387353
child 69313 b021008c5397