src/HOL/Algebra/Exponent.thy
changeset 30722 623d4831c8cf
parent 30242 aea5d7fa7ef5
child 31717 d1f7b6245a75