src/HOL/RealPow.thy
changeset 35144 8b8302da3a55
parent 35123 e286d5df187a
child 35216 7641e8d831d2
equal deleted inserted replaced
35143:7b2538c987e7 35144:8b8302da3a55