src/HOL/Real/RealPow.thy
changeset 18396 b3e7da94b51f
parent 15251 bb6f072c8d10
child 19279 48b527d0331b