| Sun, 23 Mar 2025 19:26:23 +0000 |
paulson |
Function space instead of image closure
|
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
|
| Tue, 31 Mar 2020 15:51:15 +0200 |
nipkow |
cleaned proofs
|
file |
diff |
annotate
|
| Mon, 02 Dec 2019 22:40:16 -0500 |
immler |
split off metric spaces part of Function_Topology: subsequent theories Product_Topology, T1_Spaces, Lindelof_Spaces are purely topological
|
file |
diff |
annotate
|
| Thu, 28 Nov 2019 23:06:22 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Thu, 28 Nov 2019 18:40:39 +0100 |
nipkow |
reduced imports
|
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, 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, 08 Apr 2019 15:26:54 +0100 |
paulson |
First tranche of the Homology development: Simplices
|
file |
diff |
annotate
|
| Mon, 01 Apr 2019 17:02:43 +0100 |
paulson |
A few results in Algebra, and bits for Analysis
|
file |
diff |
annotate
|
| Wed, 27 Mar 2019 14:08:26 +0000 |
paulson |
more stuff from HOL Light: Euclidean spaces and n-spheres, Hausdorff spaces, etc.
|
file |
diff |
annotate
|