src/HOL/Real/ContNotDenum.thy
changeset 23563 42f2f90b51a6
parent 23461 9a586e80ce15
child 27368 9f90ac19e32b
equal deleted inserted replaced
23562:6cad6b400cfd 23563:42f2f90b51a6