src/HOL/Real/RealPow.thy
changeset 15153 3f3926337c39
parent 15140 322485b816ac
child 15229 1eb23f805c06