src/HOL/Algebra/Exponent.thy
changeset 62020 5d208fd2507d
parent 61382 efac889fccbc
child 62348 9a5f43dac883