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