src/HOL/Algebra/Exponent.thy
changeset 72425 d0937d55eb90
parent 66453 cc19f7ca2ed6