src/HOL/Algebra/Exponent.thy
changeset 14631 ec1e67f88f49
parent 13870 cf947d1ec5ff
child 14706 71590b7733b7