src/HOL/GroupTheory/Exponent.thy
changeset 13145 59bc43b51aa2
parent 11394 e88c2c89f98e
child 13583 5fcc8bf538ee