src/HOL/Real/RealPow.thy
changeset 21530 9e2ff9d4b2b0
parent 20634 45fe31e72391
child 22624 7a6c8ed516ab