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