src/HOL/Real.thy
changeset 63412 def97df48390
parent 63353 176d1f408696
child 63494 ac0a3b9c6dae