src/HOL/Algebra/Exponent.thy
changeset 59000 6eb0725503fc
parent 58917 a3be9a47e2d7
child 59667 651ea265d568