src/HOL/RealDef.thy
changeset 36970 fb3fdb4b585e
parent 36941 fdefcbcb2887
child 36977 71c8973a604b