src/HOL/Algebra/Exponent.thy
changeset 29609 a010aab5bed0
parent 27717 21bbd410ba04
child 30011 cc264a9a033d
child 30240 5b25fee0362c