src/HOL/Real.thy
changeset 63433 aa03b0487bf5
parent 63353 176d1f408696
child 63494 ac0a3b9c6dae