src/HOL/Real/ContNotDenum.thy
2007-06-21 wenzelm 2007-06-21 tuned;
2007-06-14 wenzelm 2007-06-14 tuned proofs: avoid implicit prems;
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-09-20 huffman 2006-09-20 change section to subsection
2006-06-02 wenzelm 2006-06-02 misc cleanup;
2006-02-12 kleing 2006-02-12 * include generalised MVT in HyperReal (contributed by Benjamin Porter) * add non-denumerability of continuum in Real, includes closed intervals on real (contributed by Benjamin Porter, #22 in http://www.cs.ru.nl/~freek/100/)