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