src/HOL/RealPow.thy
changeset 36800 59b50c691b75
parent 36777 be5461582d0f
child 36821 9207505d1ee5