src/HOL/RealDef.thy
changeset 35144 8b8302da3a55
parent 35050 9f841f20dca6
child 35216 7641e8d831d2