src/HOL/Algebra/Exponent.thy
changeset 81134 d23f5a898084
parent 66453 cc19f7ca2ed6