src/HOL/Real/RealPow.thy
changeset 13936 d3671b878828
parent 12018 ec054019c910
child 14265 95b42e69436c