src/HOL/Algebra/Exponent.thy
changeset 55401 f33536723999
parent 55157 06897ea77f78
child 57512 cc97b347b301