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