src/HOL/GroupTheory/Exponent.ML
changeset 12207 4dff931b852f
parent 12196 a3be6b3a9c0b