| 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
|
| Sun, 03 Mar 2024 16:18:06 +0100 |
wenzelm |
tuned proof: avoid z3 to make it work on arm64-linux;
|
file |
diff |
annotate
|
| Wed, 24 Jan 2024 23:53:51 +0100 |
wenzelm |
tuned proof: avoid z3 to make it work on arm64-linux;
|
file |
diff |
annotate
|
| Sun, 26 Feb 2023 21:17:39 +0000 |
paulson |
Simplified some proofs
|
file |
diff |
annotate
|
| Thu, 23 Feb 2023 16:17:04 +0000 |
paulson |
has_sum now an infix operator!!
|
file |
diff |
annotate
|
| Thu, 23 Feb 2023 15:21:14 +0000 |
paulson |
New material contributed by Manuel
|
file |
diff |
annotate
|
| Tue, 17 Jan 2023 16:08:54 +0100 |
wenzelm |
backed out changeset 7f7d5c93e36b: no longer required thanks to 9096703ed99e;
|
file |
diff |
annotate
|
| Sun, 15 Jan 2023 20:00:22 +0100 |
wenzelm |
proper theory context for formal citations;
|
file |
diff |
annotate
|
| Sun, 15 Jan 2023 18:30:18 +0100 |
wenzelm |
isabelle update -u cite;
|
file |
diff |
annotate
|
| Mon, 09 Jan 2023 17:16:04 +0000 |
paulson |
Substantial de-applying and streamlining
|
file |
diff |
annotate
|
| Tue, 24 May 2022 16:21:49 +0100 |
paulson |
Renamed the misleading has_field_derivative_iff_has_vector_derivative. Inserted a number of minor lemmas
|
file |
diff |
annotate
|
| Mon, 15 Nov 2021 18:04:07 +0100 |
Manuel Eberl |
more material for HOL-Analysis.Infinite_Sum
|
file |
diff |
annotate
|
| Sat, 30 Oct 2021 19:58:45 +0200 |
wenzelm |
tuned proofs -- avoid z3, which is unavailable on arm64-linux;
|
file |
diff |
annotate
|
| Sat, 30 Oct 2021 17:10:10 +0200 |
wenzelm |
tuned proofs -- avoid z3, which is unavailable on arm64-linux;
|
file |
diff |
annotate
|
| Wed, 06 Oct 2021 14:19:46 +0200 |
eberlm |
new notion of infinite sums in HOL-Analysis, ordering on complex numbers
|
file |
diff |
annotate
|