src/HOL/Algebra/Exponent.thy
changeset 79053 badb3da19ac6
parent 66453 cc19f7ca2ed6