src/HOL/Real/RealPow.thy
changeset 26152 cf2cccf17d6d
parent 25875 536dfdc25e0a
child 26565 522f45a8604e