src/HOL/RealPow.thy
changeset 36066 1493b43204e9
parent 35632 61fd75e33137
child 36777 be5461582d0f