src/HOL/Algebra/FiniteProduct.thy
changeset 38286 c9c7bd836894
parent 35849 b5522b51cb1e
child 40786 0a54cfc9add3