| Wed, 06 Jan 2016 12:18:53 +0100 |
hoelzl |
add the proof of the central limit theorem
|
file |
diff |
annotate
|
| Wed, 30 Dec 2015 11:37:29 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Thu, 17 Dec 2015 16:43:36 +0100 |
hoelzl |
moved some theorems from the CLT proof; reordered some theorems / notation
|
file |
diff |
annotate
|
| Thu, 05 Nov 2015 10:39:49 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| 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
|