| Thu, 08 Nov 2018 09:11:52 +0100 |
haftmann |
removed relics of ASCII syntax for indexed big operators
|
file |
diff |
annotate
|
| Thu, 30 Aug 2018 17:20:54 +0200 |
Manuel Eberl |
Some basic materials on filters and topology
|
file |
diff |
annotate
|
| Thu, 17 Aug 2017 14:52:56 +0200 |
eberlm |
Replaced subseq with strict_mono
|
file |
diff |
annotate
|
| Thu, 15 Sep 2016 16:07:20 +0200 |
immler |
Liminf/Limsup and filtermap
|
file |
diff |
annotate
|
| Thu, 14 Apr 2016 15:48:11 +0200 |
hoelzl |
Probability: move emeasure and nn_integral from ereal to ennreal
|
file |
diff |
annotate
|
| Wed, 16 Mar 2016 11:49:56 +0100 |
hoelzl |
generalized some Borel measurable statements to support ennreal
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:56 +0100 |
haftmann |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
file |
diff |
annotate
|
| Mon, 04 Jan 2016 17:45:36 +0100 |
eberlm |
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
|
file |
diff |
annotate
|
| Wed, 30 Dec 2015 11:21:54 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 29 Dec 2015 23:04:53 +0100 |
wenzelm |
more symbols;
|
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
|
| Wed, 09 Dec 2015 17:35:22 +0000 |
paulson |
sorted out eventually_mono
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 16:44:26 +0000 |
paulson |
Cauchy's integral formula for circles. Starting to fix eventually_mono.
|
file |
diff |
annotate
|
| Sat, 21 Nov 2015 20:57:24 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Thu, 05 Nov 2015 10:39:49 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 16:54:31 +0200 |
hoelzl |
prove Liminf_inverse_ereal
|
file |
diff |
annotate
|
| Wed, 17 Jun 2015 11:03:05 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:20:45 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Wed, 19 Mar 2014 18:47:22 +0100 |
haftmann |
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 22:11:46 +0100 |
haftmann |
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 09:45:00 +0100 |
hoelzl |
restrict Limsup and Liminf to complete lattices
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 09:44:57 +0100 |
hoelzl |
generalize SUP and INF to the syntactic type classes Sup and Inf
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 22:04:23 +0200 |
wenzelm |
tuned proofs -- less guessing;
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 01:12:40 +0200 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file |
diff |
annotate
|
| Tue, 27 Aug 2013 16:06:27 +0200 |
hoelzl |
renamed inner_dense_linorder to dense_linorder
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 20:02:02 +0100 |
wenzelm |
tuned imports;
|
file |
diff |
annotate
|
| Tue, 05 Mar 2013 15:43:08 +0100 |
hoelzl |
move Liminf / Limsup lemmas on complete_lattices to its own file
|
file |
diff |
annotate
|