src/HOL/Algebra/Exponent.thy
changeset 24616 fac3dd4ade83
parent 23976 9a1859635978
child 24742 73b8b42a36b6