src/HOL/Algebra/Exponent.thy
changeset 27094 2cf13a72e170
parent 25162 ad4d5365d9d8
child 27105 5f139027c365