src/HOL/Algebra/Exponent.thy
changeset 17877 67d5ab1cb0d8
parent 16733 236dfafbeb63
child 20282 49c312eaaa11