src/HOL/RealPow.thy
changeset 28987 dc0ab579a5ca
parent 28952 15a4b2cf8c34
child 29667 53103fc8ffa3
equal deleted inserted replaced
28986:1ff53ff7041d 28987:dc0ab579a5ca