src/HOL/Algebra/Exponent.thy
changeset 24111 20e74aa5f56b
parent 23976 9a1859635978
child 24742 73b8b42a36b6