src/HOL/Algebra/Exponent.thy
changeset 27885 76b51cd0a37c
parent 27717 21bbd410ba04
child 30011 cc264a9a033d
child 30240 5b25fee0362c