src/HOL/GroupTheory/Coset.thy
changeset 12216 dda8c04a8fb4
parent 11394 e88c2c89f98e
child 13583 5fcc8bf538ee