src/HOL/Algebra/Exponent.thy
changeset 14151 b8bb6a6a2c46
parent 13870 cf947d1ec5ff
child 14706 71590b7733b7