| Wed, 16 Apr 2025 21:13:27 +0100 |
paulson |
tidied more proofs
|
file |
diff |
annotate
|
| Wed, 11 Oct 2023 17:02:33 +0100 |
paulson |
atin now an abbreviation for atin_within, which has been moved to Abstract_Limits
|
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
|
| 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
|
| Thu, 28 Nov 2019 23:06:22 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Fri, 14 Jun 2019 08:34:27 +0000 |
haftmann |
removed relics of ASCII syntax for indexed big operators
|
file |
diff |
annotate
|
| Fri, 05 Apr 2019 15:02:46 +0100 |
paulson |
Free_Abelian_Groups finally working; fixed some duplicates; cleaned up some proofs
|
file |
diff |
annotate
|
| Mon, 01 Apr 2019 17:02:43 +0100 |
paulson |
A few results in Algebra, and bits for Analysis
|
file |
diff |
annotate
|
| Thu, 07 Mar 2019 16:59:12 +0000 |
paulson |
renamed the constant "limit" as it is too "generic"
|
file |
diff |
annotate
|
| Thu, 07 Mar 2019 14:08:05 +0000 |
paulson |
new material for Analysis
|
file |
diff |
annotate
|