src/HOL/Algebra/Exponent.thy
changeset 58839 ccda99401bc8
parent 57865 dcfb33c26f50
child 58917 a3be9a47e2d7