| Mon, 18 Aug 2025 22:37:21 +0100 |
paulson |
Simple facts about Lebesgue integration
|
file |
diff |
annotate
|
| Fri, 08 Aug 2025 16:46:03 +0100 |
paulson |
Generalised a theorem about Lebesgue integration
|
file |
diff |
annotate
|
| Fri, 18 Oct 2024 14:37:09 +0200 |
wenzelm |
clarified syntax declarations: keep things together;
|
file |
diff |
annotate
|
| Fri, 18 Oct 2024 14:20:09 +0200 |
wenzelm |
more inner-syntax markup;
|
file |
diff |
annotate
|
| Wed, 09 Oct 2024 23:38:29 +0200 |
wenzelm |
more inner-syntax markup;
|
file |
diff |
annotate
|
| Wed, 02 Oct 2024 10:35:44 +0200 |
wenzelm |
more inner syntax markup: HOL-Analysis;
|
file |
diff |
annotate
|
| Fri, 20 Sep 2024 19:51:08 +0200 |
wenzelm |
standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing;
|
file |
diff |
annotate
|
| Sun, 25 Aug 2024 21:10:01 +0200 |
wenzelm |
more markup for syntax consts;
|
file |
diff |
annotate
|
| Thu, 18 Apr 2024 13:07:34 +0100 |
paulson |
Acknowledgement of Ata Keskin for his Martingales material
|
file |
diff |
annotate
|
| Thu, 21 Mar 2024 12:47:51 +0100 |
wenzelm |
isabelle update -u cite;
|
file |
diff |
annotate
|
| Tue, 05 Mar 2024 20:20:34 +0100 |
wenzelm |
avoid suspicious Unicode;
|
file |
diff |
annotate
|
| Tue, 05 Mar 2024 14:32:50 +0000 |
paulson |
Moving valuable library material from Martingales into the distribution
|
file |
diff |
annotate
|
| Fri, 16 Feb 2024 11:22:29 +0000 |
paulson |
Further adjustments to the syntax for Lebesgue integration
|
file |
diff |
annotate
|
| Wed, 14 Feb 2024 15:33:45 +0000 |
paulson |
the syntax of Lebesgue integrals (LINT, LBINT, ∫, etc.) now requires parentheses
|
file |
diff |
annotate
|
| Mon, 20 Feb 2023 15:19:53 +0000 |
paulson |
Replacing z powr of_int i by z powi i and adding new material from the AFP
|
file |
diff |
annotate
|
| Fri, 24 Sep 2021 22:23:26 +0200 |
wenzelm |
tuned proofs --- avoid 'guess';
|
file |
diff |
annotate
|
| Wed, 07 Apr 2021 12:28:19 +0000 |
haftmann |
simplified definition
|
file |
diff |
annotate
|
| Fri, 19 Feb 2021 13:42:12 +0100 |
Manuel Eberl |
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
|
file |
diff |
annotate
|
| Tue, 17 Sep 2019 12:36:04 +0100 |
paulson |
A few new theorems, tidying up and deletion of obsolete material
|
file |
diff |
annotate
|
| Wed, 17 Jul 2019 14:02:42 +0100 |
paulson |
a few new lemmas and a bit of tidying
|
file |
diff |
annotate
|
| Fri, 12 Apr 2019 22:09:25 +0200 |
wenzelm |
modernized tags: default scope excludes proof;
|
file |
diff |
annotate
|
| Fri, 25 Jan 2019 02:38:26 +0000 |
Angeliki KoutsoukouArgyraki |
tagged 4 theories
|
file |
diff |
annotate
|
| Tue, 01 Jan 2019 21:47:27 +0100 |
wenzelm |
more antiquotations -- less LaTeX macros;
|
file |
diff |
annotate
|
| Sun, 18 Nov 2018 18:07:51 +0000 |
haftmann |
removed legacy input syntax
|
file |
diff |
annotate
|
| Sun, 21 Oct 2018 23:02:52 +0100 |
Angeliki KoutsoukouArgyraki |
tagged 8 theories for the Analysis manual.
|
file |
diff |
annotate
|
| Sat, 04 Aug 2018 01:03:39 +0200 |
eberlm |
Small lemmas about analysis
|
file |
diff |
annotate
|
| Wed, 06 Jun 2018 18:19:55 +0200 |
nipkow |
reorient -> split; documented split
|
file |
diff |
annotate
|
| Thu, 26 Apr 2018 19:51:32 +0200 |
nipkow |
new simp modifier: reorient
|
file |
diff |
annotate
|
| Fri, 13 Apr 2018 15:58:27 +0100 |
paulson |
Probability builds with new definitions
|
file |
diff |
annotate
|
| Wed, 11 Apr 2018 16:34:44 +0100 |
paulson |
replacement of set integral abbreviations by actual definitions!
|
file |
diff |
annotate
|