src/HOL/Algebra/FiniteProduct.thy
changeset 23719 ccd9cb15c062
parent 23350 50c5b0912a0c
child 23746 a455e69c31cc