src/HOL/RealDef.thy
changeset 43168 467d5b34e1f5
parent 42311 eb32a8474a57
child 43732 6b2bdc57155b
equal deleted inserted replaced
43167:839f599bc7ed 43168:467d5b34e1f5