src/HOL/Algebra/Exponent.thy
changeset 69069 b9aca3b9619f
parent 66453 cc19f7ca2ed6