src/HOL/PReal.thy
changeset 36229 c95fab3f9cc5
parent 35372 ca158c7b1144
child 36696 1b69f78be286
equal deleted inserted replaced
36228:df47dc6c0e03 36229:c95fab3f9cc5