src/HOL/Real/ContNotDenum.thy
changeset 23433 c2c10abd2a1e
parent 23389 aaca6a8e5414
child 23461 9a586e80ce15