Wed, 17 Jun 2015 11:03:05 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
Fri, 29 May 2015 14:35:59 +0100 |
paulson |
uncountability: open interval equivalences
|
file |
diff |
annotate
|
Wed, 01 Apr 2015 16:04:21 +0100 |
paulson |
Theorem "arctan" is no longer a default simprule
|
file |
diff |
annotate
|
Mon, 16 Mar 2015 16:59:59 +0100 |
wenzelm |
proper headers;
|
file |
diff |
annotate
|
Sun, 02 Nov 2014 17:20:45 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
Wed, 11 Jun 2014 13:39:38 +0200 |
hoelzl |
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
|
file |
diff |
annotate
|
Tue, 29 Apr 2014 22:50:55 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
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
|