src/HOL/Algebra/FiniteProduct.thy
changeset 18328 841261f303a1
parent 16638 3dc904d93767
child 20318 0e0ea63fe768