src/HOL/RealDef.thy
changeset 36352 f71978e47cd5
parent 36349 39be26d1bc28
child 36409 d323e7773aa8
equal deleted inserted replaced
36351:85ee44388f7b 36352:f71978e47cd5