src/HOL/Algebra/Exponent.thy
changeset 29270 0eade173f77e
parent 27717 21bbd410ba04
child 30011 cc264a9a033d
child 30240 5b25fee0362c