src/HOL/RealDef.thy
changeset 51487 f4bfdee99304
parent 51375 d9e62d9c98de
child 51518 6a56b7088a6a