src/HOL/Algebra/Exponent.thy
changeset 22175 d9e3e4c30d6b
parent 21256 47195501ecf7
child 23976 9a1859635978
equal deleted inserted replaced
22174:f2bf6bcd4a98 22175:d9e3e4c30d6b