src/HOL/GroupTheory/DirProd.thy
changeset 11979 0a3dace545c5
parent 11394 e88c2c89f98e
child 12459 6978ab7cac64