src/HOL/Real.thy
changeset 65512 9fd620f2fa7d
parent 64267 b9a1486e79be
child 65885 77d922eff5ac
equal deleted inserted replaced
65511:ea42dfd95ec8 65512:9fd620f2fa7d