src/HOL/Algebra/Exponent.thy
changeset 14024 213dcc39358f
parent 13870 cf947d1ec5ff
child 14706 71590b7733b7