src/HOL/RealPow.thy
changeset 35437 fe196f61b970
parent 35348 c6331256b087
child 35442 992f9cb60b25