src/HOL/Algebra/Exponent.thy
changeset 14360 e654599b114e
parent 13870 cf947d1ec5ff
child 14706 71590b7733b7