src/HOL/Library/ContNotDenum.thy
Wed, 18 Dec 2013 11:53:40 +0100 hoelzl modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
Tue, 05 Nov 2013 09:45:02 +0100 hoelzl move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
Mon, 02 Sep 2013 23:35:58 +0200 wenzelm tuned proof;
Mon, 22 Nov 2010 10:34:33 +0100 hoelzl Replace surj by abbreviation; remove surj_on.
Mon, 12 Jul 2010 08:58:13 +0200 haftmann dropped superfluous [code del]s
Mon, 23 Mar 2009 08:14:24 +0100 haftmann Main is (Complex_Main) base entry point in library theories
Wed, 10 Dec 2008 10:23:47 +0100 nipkow moved ContNotDenum into Library
less more (0) tip