src/HOL/Real.thy
changeset 54614 689398f0953f
parent 54489 03ff4d1e6784
child 54863 82acc20ded73
equal deleted inserted replaced
54613:985f8b49c050 54614:689398f0953f