src/HOL/Real/RealDef.ML
changeset 10017 e146bbfc38c1
parent 9969 4753185f1dd2
child 10043 a0364652e115