| 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
|