src/HOL/Algebra/Exponent.thy
changeset 25563 cab4f808f791
parent 25162 ad4d5365d9d8
child 27105 5f139027c365