| 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
|
| Fri, 30 Aug 2024 10:16:48 +0100 |
paulson |
More tidying of old proofs
|
file |
diff |
annotate
|
| Sun, 11 Feb 2024 12:52:14 +0000 |
paulson |
new lemmas involving Ramsey numbers, infinite sets
|
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
|
| Mon, 26 Jun 2023 14:38:19 +0100 |
paulson |
New and generalised analysis lemmas
|
file |
diff |
annotate
|
| Tue, 31 Jan 2023 14:05:16 +0000 |
paulson |
Lots more new material thanks to Manuel Eberl
|
file |
diff |
annotate
|
| Thu, 24 Mar 2022 22:43:41 +0000 |
paulson |
Some new library lemmas
|
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
|
| Sat, 23 May 2020 21:24:33 +0100 |
paulson |
a few new lemmas about functions
|
file |
diff |
annotate
|
| Wed, 04 Dec 2019 12:44:38 +0000 |
paulson |
two new theorems
|
file |
diff |
annotate
|
| Tue, 12 Nov 2019 12:33:05 +0000 |
paulson |
New library material from the AFP entry ZFC_in_HOL
|
file |
diff |
annotate
|
| Thu, 07 Mar 2019 14:08:05 +0000 |
paulson |
new material for Analysis
|
file |
diff |
annotate
|
| Thu, 24 Jan 2019 14:44:52 +0000 |
paulson |
the theory of Equipollence, and moving Fpow from Cardinals into Main
|
file |
diff |
annotate
|