src/HOL/Algebra/Exponent.thy
changeset 26191 ae537f315b34
parent 25162 ad4d5365d9d8
child 27105 5f139027c365