src/HOL/RealDef.thy
changeset 33689 d0a9ce721e0c
parent 33657 a4179bf442d1
child 35028 108662d50512
equal deleted inserted replaced
33688:1a97dcd8dc6a 33689:d0a9ce721e0c