src/HOL/RealDef.thy
changeset 40858 69ab03d29c92
parent 40826 a3af470a55d2
child 40864 4abaaadfdaf2