src/HOL/RealPow.thy
changeset 30458 804de935c328
parent 30273 ecd6f0ca62ea
child 30960 fec1a04b7220
equal deleted inserted replaced
30457:28b487cd9e15 30458:804de935c328