src/HOL/Algebra/Exponent.thy
changeset 34059 f3f0e20923a7
parent 32946 22664da2923b
child 35848 5443079512ea