src/HOL/RealDef.thy
changeset 46962 5bdcdb28be83
parent 46670 e9aa6d151329
child 47108 2a1953f0d20d
equal deleted inserted replaced
46960:f19e5837ad69 46962:5bdcdb28be83