src/HOL/Real/ContNotDenum.thy
changeset 21199 2d83f93c3580
parent 20635 e95db20977c5
child 21404 eb85850d3eb7
equal deleted inserted replaced
21198:48b8d8b8334d 21199:2d83f93c3580