src/HOL/Real/RealPow.thy
changeset 21966 edab0ecfbd7c
parent 20634 45fe31e72391
child 22624 7a6c8ed516ab