src/HOL/Real.thy
changeset 36832 e6078ef937df
parent 35090 88cc65ae046e
child 36899 bcd6fce5bf06
equal deleted inserted replaced
36831:3037d6810fca 36832:e6078ef937df