src/HOL/Algebra/Exponent.thy
changeset 30424 692279df7cc2
parent 30242 aea5d7fa7ef5
child 31717 d1f7b6245a75