| Thu, 03 Jul 2025 13:53:14 +0200 |
nipkow |
removed duplicate lemma; added the notion of the kernel of a function
|
file |
diff |
annotate
|
| Tue, 22 Apr 2025 17:35:02 +0100 |
paulson |
More tidying and some variable renaming
|
file |
diff |
annotate
|
| Wed, 09 Oct 2024 23:38:29 +0200 |
wenzelm |
more inner-syntax markup;
|
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
|
| Tue, 23 May 2023 12:31:23 +0100 |
paulson |
Finally, the abstract metric space development
|
file |
diff |
annotate
|
| Thu, 02 Feb 2023 12:55:07 +0000 |
paulson |
More of Manuel's material, and some changes
|
file |
diff |
annotate
|
| Sat, 31 Dec 2022 11:09:19 +0000 |
paulson |
repaired a proof
|
file |
diff |
annotate
|
| Fri, 30 Dec 2022 17:48:41 +0000 |
paulson |
A further round of proof consolidation
|
file |
diff |
annotate
|
| Thu, 29 Dec 2022 22:14:12 +0000 |
paulson |
More tidying
|
file |
diff |
annotate
|
| Wed, 27 Oct 2021 11:47:42 +0100 |
paulson |
moved a theorem to a sensible place
|
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
|
| Thu, 14 May 2020 13:44:44 +0200 |
Manuel Eberl |
Tuned some proofs in HOL-Analysis
|
file |
diff |
annotate
|
| Tue, 31 Mar 2020 15:51:15 +0200 |
nipkow |
cleaned proofs
|
file |
diff |
annotate
|
| Wed, 18 Sep 2019 14:41:37 +0100 |
paulson |
imported new material mostly due to Sébastien Gouëzel
|
file |
diff |
annotate
|
| Tue, 17 Sep 2019 16:21:31 +0100 |
paulson |
A couple of new theorems, stolen from AFP entries
|
file |
diff |
annotate
|
| Tue, 27 Aug 2019 17:08:51 +0200 |
nipkow |
moved lemmas
|
file |
diff |
annotate
|
| Thu, 15 Aug 2019 16:11:56 +0100 |
paulson |
new material; rotated premises of Lim_transform_eventually
|
file |
diff |
annotate
|
| Thu, 18 Jul 2019 15:40:15 +0100 |
paulson |
More analysis / measure theory material
|
file |
diff |
annotate
|
| Fri, 12 Apr 2019 22:09:25 +0200 |
wenzelm |
modernized tags: default scope excludes proof;
|
file |
diff |
annotate
|
| Tue, 05 Mar 2019 07:00:21 +0000 |
haftmann |
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
|
file |
diff |
annotate
|
| Mon, 14 Jan 2019 18:35:03 +0000 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Tue, 01 Jan 2019 21:47:27 +0100 |
wenzelm |
more antiquotations -- less LaTeX macros;
|
file |
diff |
annotate
|
| Tue, 01 Jan 2019 13:26:37 +0100 |
nipkow |
tuned defs
|
file |
diff |
annotate
|
| Sun, 30 Dec 2018 10:34:56 +0000 |
haftmann |
prefer naming convention from datatype package for strong congruence rules
|
file |
diff |
annotate
|
| Sat, 29 Dec 2018 17:46:48 +0100 |
immler |
tuned analysis manual
|
file |
diff |
annotate
|
| Fri, 28 Dec 2018 10:29:59 +0100 |
nipkow |
tuned style and headers
|
file |
diff |
annotate
|
| Sun, 18 Nov 2018 18:07:51 +0000 |
haftmann |
removed legacy input syntax
|
file |
diff |
annotate
|