src/HOL/Real/ContNotDenum.thy
changeset 23719 ccd9cb15c062
parent 23461 9a586e80ce15
child 27368 9f90ac19e32b
equal deleted inserted replaced
23718:8ff68cb5860c 23719:ccd9cb15c062