src/HOL/GroupTheory/Exponent.ML
changeset 13145 59bc43b51aa2
parent 12196 a3be6b3a9c0b