src/HOL/Real/RealPow.ML
changeset 10689 5c44de6aadf4
parent 10677 36625483213f
child 10690 cd80241125b0