src/HOL/Algebra/Exponent.thy
changeset 31232 689aa7da48cc
parent 30242 aea5d7fa7ef5
child 31717 d1f7b6245a75