src/HOL/Algebra/Product_Groups.thy
changeset 78134 a11ebc8c751a
parent 73932 fd21b4a93043