src/HOL/Algebra/Exponent.thy
changeset 31796 117300d72398
parent 31717 d1f7b6245a75
child 31952 40501bb2d57c