src/HOL/Real/RealPow.thy
changeset 17184 3d80209e9a53
parent 15251 bb6f072c8d10
child 19279 48b527d0331b