src/HOL/Algebra/FiniteProduct.thy
changeset 21955 c1a6fad248ca
parent 20318 0e0ea63fe768
child 22265 3c5c6bdf61de