src/HOL/RealDef.thy
changeset 43016 42330f25142c
parent 42311 eb32a8474a57
child 43732 6b2bdc57155b
equal deleted inserted replaced
43015:21b6baec55b1 43016:42330f25142c