src/HOL/Algebra/Exponent.thy
changeset 70443 a21a96eda033
parent 66453 cc19f7ca2ed6