src/HOL/Algebra/Exponent.thy
changeset 30278 18ce07e05a95
parent 30242 aea5d7fa7ef5
child 31717 d1f7b6245a75