src/HOL/RealDef.thy
changeset 34917 51829fe604a7
parent 33657 a4179bf442d1
child 35028 108662d50512
equal deleted inserted replaced
34906:bb9dad7de515 34917:51829fe604a7