src/HOL/RealDef.thy
changeset 30079 293b896b9c25
parent 30042 31039ee583fa
child 30082 43c5b7bfc791