| Wed, 23 Apr 2025 01:38:06 +0200 |
Manuel Eberl |
some material on power series and infinite products
|
file |
diff |
annotate
|
| Fri, 18 Apr 2025 12:26:04 +0200 |
Manuel Eberl |
some facts about power series
|
file |
diff |
annotate
|
| Fri, 18 Apr 2025 10:58:16 +0200 |
Manuel Eberl |
moved some lemmas to where they fit better
|
file |
diff |
annotate
|
| Tue, 15 Apr 2025 15:17:25 +0200 |
Manuel Eberl |
new lemmas for HOL-Complex_Analysis; overhaul of isolated_zeros
|
file |
diff |
annotate
|
| Thu, 10 Apr 2025 17:07:18 +0100 |
paulson |
A couple of new lemmas
|
file |
diff |
annotate
|
| Mon, 24 Mar 2025 21:24:03 +0000 |
paulson |
New material by Manuel Eberl
|
file |
diff |
annotate
|
| Thu, 26 Sep 2024 14:44:37 +0100 |
paulson |
To tiny but maybe useful lemmas (moved in from the AFP, Word_Lib)
|
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
|
| Thu, 21 Mar 2024 14:19:39 +0000 |
paulson |
New material from a variety of sources (including AFP)
|
file |
diff |
annotate
|
| Thu, 12 Oct 2023 12:36:09 +0100 |
paulson |
Fixed the duplication of fls_compose_fps, moving the definition in Laurent_Convergence to Formal_Laurent_Series along with several simpler facts
|
file |
diff |
annotate
|
| Wed, 27 Sep 2023 13:34:15 +0100 |
paulson |
Importing or moving a few more useful theorems
|
file |
diff |
annotate
|
| Mon, 21 Aug 2023 18:38:25 +0100 |
paulson |
Numerous minor tweaks and simplifications
|
file |
diff |
annotate
|
| Mon, 20 Feb 2023 15:19:53 +0000 |
paulson |
Replacing z powr of_int i by z powi i and adding new material from the AFP
|
file |
diff |
annotate
|
| Thu, 16 Feb 2023 12:21:21 +0000 |
paulson |
More of Eberl's contributions: memomorphic functions
|
file |
diff |
annotate
|