src/HOL/RealPow.thy
changeset 36817 ed97e877ff2d
parent 36777 be5461582d0f
child 36821 9207505d1ee5