src/HOL/Algebra/Exponent.thy
changeset 58078 d44c9dc4bf30
parent 57865 dcfb33c26f50
child 58917 a3be9a47e2d7