| Wed, 16 Apr 2025 21:13:27 +0100 |
paulson |
tidied more proofs
|
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
|
| Sat, 23 Sep 2023 18:45:19 +0100 |
paulson |
A few new or simplified proofs
|
file |
diff |
annotate
|
| Sat, 15 Jul 2023 23:34:42 +0100 |
paulson |
trivial_topology
|
file |
diff |
annotate
|
| Tue, 11 Jul 2023 20:21:58 +0100 |
paulson |
cosmetic improvements, new lemmas, especially more uses of function space
|
file |
diff |
annotate
|
| Wed, 05 Jul 2023 16:50:07 +0100 |
paulson |
A couple of new lemmas involving cardinality
|
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, 03 Jul 2023 11:45:59 +0100 |
paulson |
EXPERIMENTAL replacement of f ` A <= B by f : A -> B in Analysis
|
file |
diff |
annotate
|
| Mon, 26 Jun 2023 14:38:19 +0100 |
paulson |
New and generalised analysis lemmas
|
file |
diff |
annotate
|
| Mon, 15 May 2023 17:12:18 +0100 |
paulson |
More material from the HOL Light metric space library
|
file |
diff |
annotate
|
| Sun, 07 May 2023 14:52:53 +0100 |
paulson |
Importation of additional lemmas from metric.ml
|
file |
diff |
annotate
|
| Tue, 02 May 2023 12:51:05 +0100 |
paulson |
A few new theorems
|
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
|
| Tue, 03 Jan 2023 17:02:41 +0000 |
paulson |
More tidying of proofs
|
file |
diff |
annotate
|
| Fri, 24 Sep 2021 22:23:26 +0200 |
wenzelm |
tuned proofs --- avoid 'guess';
|
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, 29 Aug 2020 16:30:22 +0100 |
paulson |
quite a bit of tidying
|
file |
diff |
annotate
|
| Wed, 13 May 2020 16:35:36 +0200 |
Manuel Eberl |
new HOL simproc: eliminate_false_implies
|
file |
diff |
annotate
|
| Fri, 29 Nov 2019 15:06:04 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Thu, 28 Nov 2019 23:06:22 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Wed, 17 Apr 2019 17:48:28 +0100 |
paulson |
Lindelöf spaces and supporting material
|
file |
diff |
annotate
|
| Fri, 12 Apr 2019 22:09:25 +0200 |
wenzelm |
modernized tags: default scope excludes proof;
|
file |
diff |
annotate
|
| Thu, 21 Mar 2019 14:18:22 +0000 |
paulson |
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
|
file |
diff |
annotate
|
| Tue, 19 Mar 2019 16:14:51 +0000 |
paulson |
new material about topology, etc.; also fixes for yesterday's
|
file |
diff |
annotate
|
| Tue, 29 Jan 2019 21:56:40 +0100 |
wenzelm |
eliminated suspicious Unicode;
|
file |
diff |
annotate
|
| Tue, 29 Jan 2019 16:13:11 +0100 |
nipkow |
moved generalized material
|
file |
diff |
annotate
|
| Mon, 07 Jan 2019 18:50:41 +0100 |
immler |
moved generalized lemmas
|
file |
diff |
annotate
|
| Mon, 07 Jan 2019 13:08:50 +0100 |
immler |
split off theory combining Elementary_Topology and Abstract_Topology
|
file |
diff |
annotate
|