| Mon, 03 Jul 2023 11:45:59 +0100 |
paulson |
EXPERIMENTAL replacement of f ` A <= B by f : A -> B in Analysis
|
file |
diff |
annotate
|
| Thu, 01 Jun 2023 12:08:33 +0100 |
paulson |
Even more material from the HOL Light metric space library
|
file |
diff |
annotate
|
| Tue, 17 May 2022 14:10:14 +0100 |
paulson |
tidied auto / simp with null arguments
|
file |
diff |
annotate
|
| Mon, 06 Apr 2020 11:56:04 +0100 |
paulson |
fixed a broken frac_le proof
|
file |
diff |
annotate
|
| Tue, 31 Mar 2020 15:51:15 +0200 |
nipkow |
cleaned proofs
|
file |
diff |
annotate
|
| Fri, 29 Nov 2019 15:06:04 +0100 |
nipkow |
tuned
|
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
|
| Tue, 27 Aug 2019 22:43:19 +0200 |
immler |
fixed typo
|
file |
diff |
annotate
|
| Tue, 27 Aug 2019 22:41:47 +0200 |
immler |
moved lemmas; reduced dependencies of Lipschitz
|
file |
diff |
annotate
|
| Fri, 12 Apr 2019 22:09:25 +0200 |
wenzelm |
modernized tags: default scope excludes proof;
|
file |
diff |
annotate
|
| Tue, 01 Jan 2019 21:47:27 +0100 |
wenzelm |
more antiquotations -- less LaTeX macros;
|
file |
diff |
annotate
|
| Fri, 28 Dec 2018 10:29:59 +0100 |
nipkow |
tuned style and headers
|
file |
diff |
annotate
|
| Wed, 29 Aug 2018 07:50:28 +0100 |
immler |
tagged some theories
|
file |
diff |
annotate
|
| Sun, 20 May 2018 20:14:30 +0100 |
paulson |
one last fix
|
file |
diff |
annotate
|
| Sat, 14 Apr 2018 09:23:00 +0100 |
paulson |
new material about vec, real^1, etc.
|
file |
diff |
annotate
|
| Mon, 26 Feb 2018 07:34:05 +0100 |
immler |
moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements
|
file |
diff |
annotate
|