src/HOL/Real/RealPow.thy
changeset 16377 9da1cf997e79
parent 15251 bb6f072c8d10
child 19279 48b527d0331b