src/HOL/Algebra/Exponent.thy
changeset 77976 ca11a87bd2c6
parent 66453 cc19f7ca2ed6