src/HOL/Algebra/Exponent.thy
changeset 64832 f6a09ac4e640
parent 63633 2accfb71e33b
child 65417 fc41a5650fb1