src/HOL/Algebra/Exponent.thy
changeset 32389 cb3c5189ea85
parent 31952 40501bb2d57c
child 32480 6c19da8e661a