src/HOL/Real/RealPow.ML
changeset 13636 fdf7e9388be7
parent 12613 279facb4253a