src/HOL/Algebra/Exponent.thy
changeset 79039 322bcfce2b37
parent 66453 cc19f7ca2ed6