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