src/HOL/Algebra/Exponent.thy
changeset 34976 06df18c9a091
parent 32946 22664da2923b
child 35848 5443079512ea