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