| Mon, 14 Jul 2025 18:41:41 +0100 |
paulson |
A few more lemmas
|
file |
diff |
annotate
|
| Mon, 14 Jul 2025 12:33:34 +0100 |
paulson |
A number of basic and unaccountably missing lemmas about complex exponentiation
|
file |
diff |
annotate
|
| Tue, 15 Apr 2025 17:38:20 +0200 |
Manuel Eberl |
lots of lemmas for HOL, HOL-{Complex_}Analysis, HOL-Number_Theory
|
file |
diff |
annotate
|
| Tue, 08 Apr 2025 19:06:00 +0100 |
paulson |
More of Manuel's material
|
file |
diff |
annotate
|
| Mon, 24 Mar 2025 21:24:03 +0000 |
paulson |
New material by Manuel Eberl
|
file |
diff |
annotate
|
| Mon, 03 Jun 2024 20:56:21 +0100 |
paulson |
Simplification of sin, cos, exp of multiples of pi
|
file |
diff |
annotate
|
| Mon, 11 Mar 2024 15:07:02 +0000 |
paulson |
New material by Wenda Li and Manuel Eberl
|
file |
diff |
annotate
|
| Mon, 19 Feb 2024 14:12:20 +0000 |
paulson |
A small collection of new and useful facts, including the AM-GM inequality
|
file |
diff |
annotate
|
| Fri, 03 Nov 2023 16:20:06 +0000 |
paulson |
Added Kronecker's approximation theorem. Requires adding Real_Asymp to HOL-Analysis. Funny syntax issue in Probability/Projective_Family
|
file |
diff |
annotate
|
| Thu, 03 Aug 2023 19:10:36 +0200 |
paulson |
More cosmetic changes
|
file |
diff |
annotate
|
| Mon, 20 Feb 2023 17:11:43 +0000 |
paulson |
Simplified some more proofs
|
file |
diff |
annotate
|
| Fri, 17 Feb 2023 13:48:42 +0000 |
paulson |
Moved up a theorem
|
file |
diff |
annotate
|
| Thu, 16 Feb 2023 10:42:28 +0000 |
paulson |
New material due to Eberl on Formal Laurent Series
|
file |
diff |
annotate
|
| Wed, 15 Feb 2023 12:46:12 +0000 |
paulson |
A bit more tidying and some new material
|
file |
diff |
annotate
|
| Fri, 10 Feb 2023 14:51:51 +0000 |
paulson |
Some basis results about trigonometric functions
|
file |
diff |
annotate
|
| Wed, 08 Feb 2023 15:05:24 +0000 |
paulson |
Lots of new material chiefly about complex analysis
|
file |
diff |
annotate
|
| Tue, 07 Feb 2023 14:10:08 +0000 |
paulson |
More new theorems from the number theory development
|
file |
diff |
annotate
|
| Mon, 06 Feb 2023 15:41:23 +0000 |
paulson |
Some more new material and some tidying of existing proofs
|
file |
diff |
annotate
|
| Thu, 02 Feb 2023 12:55:07 +0000 |
paulson |
More of Manuel's material, and some changes
|
file |
diff |
annotate
|
| Wed, 01 Feb 2023 12:43:33 +0000 |
paulson |
More new material thanks to Manuel
|
file |
diff |
annotate
|
| Tue, 31 Jan 2023 14:05:16 +0000 |
paulson |
Lots more new material thanks to Manuel Eberl
|
file |
diff |
annotate
|
| Fri, 27 Jan 2023 13:57:52 +0000 |
paulson |
Shortened a messy proof
|
file |
diff |
annotate
|
| Wed, 25 Jan 2023 13:37:44 +0000 |
paulson |
Some new material from the AFP
|
file |
diff |
annotate
|
| Thu, 29 Dec 2022 11:46:06 +0000 |
paulson |
reorganisation and simplification of theorems about transcendental functions
|
file |
diff |
annotate
|
| Wed, 21 Dec 2022 12:30:48 +0000 |
paulson |
Additional new material about infinite products, etc.
|
file |
diff |
annotate
|
| Tue, 20 Dec 2022 17:59:44 +0000 |
paulson |
First round of moving material from the number theory development
|
file |
diff |
annotate
|
| Sun, 11 Sep 2022 13:27:39 +0100 |
paulson |
tidied a few ugly proofs
|
file |
diff |
annotate
|
| Mon, 30 May 2022 12:46:11 +0100 |
paulson |
Five slightly useful lemmas
|
file |
diff |
annotate
|
| Fri, 15 Oct 2021 12:42:51 +0100 |
paulson |
A few new lemmas plus some refinements
|
file |
diff |
annotate
|
| Thu, 08 Jul 2021 08:44:18 +0200 |
desharna |
merged
|
file |
diff |
annotate
|
| Thu, 08 Jul 2021 08:42:36 +0200 |
desharna |
added opaque_combs and renamed hide_lams to opaque_lifting
|
file |
diff |
annotate
|
| Sun, 04 Jul 2021 18:35:57 +0100 |
paulson |
Imported lots of material from Stirling_Formula/Gamma_Asymptotics
|
file |
diff |
annotate
|
| Fri, 02 Jul 2021 15:54:31 +0100 |
paulson |
converting arg to Arg
|
file |
diff |
annotate
|
| Mon, 28 Jun 2021 15:05:46 +0100 |
paulson |
A few useful lemmas about derivatives, colinearity and other topics
|
file |
diff |
annotate
|
| Fri, 25 Sep 2020 12:05:21 +0100 |
paulson |
de-applying and tidying
|
file |
diff |
annotate
|
| Tue, 31 Mar 2020 15:51:15 +0200 |
nipkow |
cleaned proofs
|
file |
diff |
annotate
|
| Sun, 01 Dec 2019 19:10:57 +0000 |
Wenda Li |
renamed Analysis/Winding_Numbers to Winding_Numbers_2; reorganised Analysis/Cauchy_Integral_Theorem by splitting it into Contour_Integration, Winding_Numbers,Cauchy_Integral_Theorem and Cauchy_Integral_Formula.
|
file |
diff |
annotate
|
| Mon, 04 Nov 2019 17:06:18 +0000 |
paulson |
Moved or deleted some out of place material, also eliminating obsolete naming conventions
|
file |
diff |
annotate
|
| Sat, 02 Nov 2019 15:52:47 +0000 |
paulson |
reorganisation to eliminate Brouwer_Fixpoint from complex analysis
|
file |
diff |
annotate
|
| Sat, 02 Nov 2019 14:31:34 +0000 |
paulson |
Inverse function theorem + lemmas
|
file |
diff |
annotate
|
| Wed, 09 Oct 2019 14:51:54 +0000 |
haftmann |
dedicated fact collections for algebraic simplification rules potentially splitting goals
|
file |
diff |
annotate
|
| Thu, 19 Sep 2019 12:36:15 +0100 |
paulson |
A few more simple results
|
file |
diff |
annotate
|
| Wed, 17 Jul 2019 16:32:06 +0100 |
paulson |
fixed renaming issues
|
file |
diff |
annotate
|
| Wed, 17 Jul 2019 14:02:42 +0100 |
paulson |
a few new lemmas and a bit of tidying
|
file |
diff |
annotate
|
| Fri, 26 Apr 2019 16:51:40 +0100 |
paulson |
Added embedding_map_into_euclideanreal; reduced dependence on Equivalence_Lebesgue_Henstock_Integration in Analysis theories by moving a few lemmas
|
file |
diff |
annotate
|
| Fri, 12 Apr 2019 22:09:25 +0200 |
wenzelm |
modernized tags: default scope excludes proof;
|
file |
diff |
annotate
|
| Tue, 26 Mar 2019 17:01:36 +0000 |
paulson |
generalised homotopic_with to topologies; homotopic_with_canon is the old version
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Tue, 01 Jan 2019 21:47:27 +0100 |
wenzelm |
more antiquotations -- less LaTeX macros;
|
file |
diff |
annotate
|
| Sat, 29 Dec 2018 15:43:53 +0100 |
nipkow |
capitalize proper names in lemma names
|
file |
diff |
annotate
|
| Thu, 27 Dec 2018 19:48:28 +0100 |
nipkow |
tuned headers; ~ -> \<not>
|
file |
diff |
annotate
|
| Mon, 22 Oct 2018 19:03:47 +0200 |
Manuel Eberl |
Tagged some theories in HOL-Analysis
|
file |
diff |
annotate
|
| Sat, 04 Aug 2018 01:03:39 +0200 |
eberlm |
Small lemmas about analysis
|
file |
diff |
annotate
|
| Tue, 03 Jul 2018 14:46:14 +0100 |
paulson |
more on infinite products
|
file |
diff |
annotate
|
| Fri, 29 Jun 2018 15:22:30 +0100 |
paulson |
The unwinding number is an integer.
|
file |
diff |
annotate
|
| Thu, 28 Jun 2018 14:13:57 +0100 |
paulson |
Generalising and renaming some basic results
|
file |
diff |
annotate
|
| Tue, 26 Jun 2018 20:48:49 +0100 |
paulson |
a few new lemmas
|
file |
diff |
annotate
|
| Tue, 26 Jun 2018 14:51:18 +0100 |
paulson |
Rationalisation of complex transcendentals, esp the Arg function
|
file |
diff |
annotate
|
| Mon, 25 Jun 2018 12:51:18 +0100 |
paulson |
Renaming Arg -> Arg2pi
|
file |
diff |
annotate
|
| Thu, 24 May 2018 21:58:17 +0100 |
paulson |
more small tidying
|
file |
diff |
annotate
|