src/HOL/Real/RealPow.thy
changeset 13757 33b84d172c97
parent 12018 ec054019c910
child 14265 95b42e69436c