src/HOL/Real/RealPow.ML
changeset 9502 50ec59aff389
parent 9428 c8eb573114de
child 10043 a0364652e115