src/HOL/Real/RealPow.ML
changeset 10017 e146bbfc38c1
parent 9428 c8eb573114de
child 10043 a0364652e115
equal deleted inserted replaced
10016:3833b58a5d88 10017:e146bbfc38c1