src/HOL/RealPow.thy
changeset 29795 c78806b621e1
parent 29667 53103fc8ffa3
child 30082 43c5b7bfc791
equal deleted inserted replaced
29794:32d00a2a6f28 29795:c78806b621e1