src/HOL/RealDef.thy
changeset 35147 9eb89f41c29d
parent 35050 9f841f20dca6
child 35216 7641e8d831d2