| Sun, 07 Jul 2024 22:25:34 +0100 |
paulson |
last-minute correction: no simprule for ln_minus
|
file |
diff |
annotate
|
| Sat, 06 Jul 2024 12:51:31 +0100 |
paulson |
Totalisation of ln and therefore log and powr
|
file |
diff |
annotate
|
| Fri, 05 Jul 2024 21:58:40 +0100 |
paulson |
The changes needed to reduce the need to snoop on edits to theory files
|
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, 13 May 2024 22:42:40 +0100 |
paulson |
More binomial material
|
file |
diff |
annotate
|
| Mon, 06 May 2024 14:39:33 +0100 |
paulson |
Some new simprules – and patches for proofs
|
file |
diff |
annotate
|
| Thu, 28 Mar 2024 13:32:57 +0000 |
paulson |
An assortment of new material, mostly due to Manuel
|
file |
diff |
annotate
|
| Wed, 27 Mar 2024 15:16:09 +0000 |
paulson |
New material and a bit of refactoring
|
file |
diff |
annotate
|
| Thu, 21 Mar 2024 14:19:39 +0000 |
paulson |
New material from a variety of sources (including AFP)
|
file |
diff |
annotate
|
| Tue, 05 Mar 2024 14:32:50 +0000 |
paulson |
Moving valuable library material from Martingales into the distribution
|
file |
diff |
annotate
|
| Wed, 21 Feb 2024 10:46:22 +0000 |
paulson |
New material about transcendental functions, polynomials, et cetera, thanks to 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
|
| Thu, 25 Jan 2024 17:08:07 +0000 |
paulson |
Three new lemmas
|
file |
diff |
annotate
|
| Tue, 16 Jan 2024 13:40:09 +0000 |
paulson |
A few new results (mostly brought in from other developments)
|
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, 19 Oct 2023 21:38:09 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 19 Oct 2023 17:06:39 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 29 Sep 2023 13:59:56 +0100 |
paulson |
A couple of new lemmas
|
file |
diff |
annotate
|
| Sat, 23 Sep 2023 18:45:19 +0100 |
paulson |
A few new or simplified proofs
|
file |
diff |
annotate
|
| Tue, 12 Sep 2023 13:54:48 +0100 |
paulson |
A little reorganisation
|
file |
diff |
annotate
|
| Sun, 09 Jul 2023 11:38:25 +0100 |
paulson |
Last of the HOL Light metric space imports, and some supporting lemmas
|
file |
diff |
annotate
|
| Tue, 04 Jul 2023 12:53:01 +0100 |
paulson |
Another tranche of HOL Light material on metric and topological spaces
|
file |
diff |
annotate
|
| Thu, 02 Mar 2023 17:17:18 +0000 |
paulson |
Some new lemmas. Some tidying up
|
file |
diff |
annotate
|
| Fri, 10 Feb 2023 14:51:51 +0000 |
paulson |
Some basis results about trigonometric functions
|
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
|
| Tue, 31 Jan 2023 14:05:16 +0000 |
paulson |
Lots more new material thanks to Manuel Eberl
|
file |
diff |
annotate
|
| Mon, 30 Jan 2023 15:24:17 +0000 |
paulson |
Moved in a large number of highly useful library lemmas, mostly due to Manuel Eberl
|
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
|
| Tue, 26 Oct 2021 14:43:59 +0000 |
haftmann |
more generic bit/word lemmas for distribution
|
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
|
| Wed, 23 Dec 2020 16:25:52 +0000 |
paulson |
default simprule for geometric series
|
file |
diff |
annotate
|
| Thu, 27 Aug 2020 15:23:48 +0100 |
paulson |
but not the [cong] rule
|
file |
diff |
annotate
|
| Thu, 27 Aug 2020 12:14:46 +0100 |
paulson |
tidying up some theorem statements
|
file |
diff |
annotate
|
| Wed, 26 Aug 2020 15:59:21 +0100 |
paulson |
tiny tidy-up of proofs
|
file |
diff |
annotate
|
| Fri, 19 Jun 2020 09:46:47 +0000 |
haftmann |
prefer single name
|
file |
diff |
annotate
|
| Thu, 04 Jun 2020 15:30:22 +0000 |
haftmann |
more simp rules
|
file |
diff |
annotate
|
| Wed, 13 May 2020 12:55:33 +0200 |
Manuel Eberl |
new constant power_int in HOL
|
file |
diff |
annotate
|
| Sun, 22 Mar 2020 17:21:16 +0000 |
paulson |
tidying up some horrible proofs
|
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
|
| Wed, 18 Sep 2019 14:41:37 +0100 |
paulson |
imported new material mostly due to Sébastien Gouëzel
|
file |
diff |
annotate
|
| Tue, 17 Sep 2019 16:21:31 +0100 |
paulson |
A couple of new theorems, stolen from AFP entries
|
file |
diff |
annotate
|
| Thu, 15 Aug 2019 16:11:56 +0100 |
paulson |
new material; rotated premises of Lim_transform_eventually
|
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, 14 Jun 2019 08:34:28 +0000 |
haftmann |
moved some theorems into HOL main corpus
|
file |
diff |
annotate
|
| Wed, 15 May 2019 12:47:15 +0100 |
paulson |
Generalisations involving numerals; comparisons should now work for ennreal
|
file |
diff |
annotate
|
| Wed, 10 Apr 2019 21:29:32 +0100 |
paulson |
Fixing the main Homology theory; also moving a lot of sum/prod lemmas into their generic context
|
file |
diff |
annotate
|
| Wed, 10 Apr 2019 13:34:55 +0100 |
paulson |
The last big tranche of Homology material: invariance of domain; renamings to use generic sum/prod lemmas from their locale
|
file |
diff |
annotate
|
| Mon, 14 Jan 2019 14:46:12 +0100 |
nipkow |
uniform naming
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 08 Nov 2018 22:29:09 +0100 |
wenzelm |
isabelle update_cartouches -t;
|
file |
diff |
annotate
|
| Sun, 21 Oct 2018 09:39:09 +0200 |
nipkow |
uniform naming of strong congruence rules
|
file |
diff |
annotate
|
| Thu, 20 Sep 2018 18:20:02 +0100 |
paulson |
removal of more redundancies, and fixes
|
file |
diff |
annotate
|
| Thu, 20 Sep 2018 14:17:58 +0100 |
paulson |
elimination of near duplication involving Rolle's theorem and the MVT
|
file |
diff |
annotate
|
| Fri, 17 Aug 2018 11:26:35 +0000 |
haftmann |
proper code abbreviation for power on real
|
file |
diff |
annotate
|
| Mon, 16 Jul 2018 15:24:06 +0200 |
Manuel Eberl |
Made simproc for sqrt/root of numeral more robust
|
file |
diff |
annotate
|
| Sun, 15 Jul 2018 21:58:50 +0100 |
paulson |
de-applying and meta-quantifying
|
file |
diff |
annotate
|
| Sun, 15 Jul 2018 16:05:38 +0100 |
paulson |
fixes and more de-applying
|
file |
diff |
annotate
|
| Sun, 15 Jul 2018 13:15:31 +0100 |
paulson |
more de-applying and a fix
|
file |
diff |
annotate
|