| Thu, 08 Jul 2021 08:44:18 +0200 |
desharna |
merged
|
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
|
| Mon, 28 Jun 2021 15:05:46 +0100 |
paulson |
A few useful lemmas about derivatives, colinearity and other topics
|
file |
diff |
annotate
|
| Wed, 11 Nov 2020 14:27:17 +0000 |
paulson |
mult_le_cancel_iff1, mult_le_cancel_iff2, mult_less_iff1 generalised from the real_ versions
|
file |
diff |
annotate
|
| Sun, 30 Aug 2020 19:45:46 +0100 |
paulson |
minor tidying, also s->S and t->T
|
file |
diff |
annotate
|
| Sat, 29 Aug 2020 16:30:22 +0100 |
paulson |
quite a bit of tidying
|
file |
diff |
annotate
|
| Tue, 31 Mar 2020 15:51:15 +0200 |
nipkow |
cleaned proofs
|
file |
diff |
annotate
|
| Mon, 02 Dec 2019 13:57:32 -0500 |
immler |
tuned Analysis manual
|
file |
diff |
annotate
|
| Mon, 02 Dec 2019 14:22:03 +0100 |
Manuel Eberl |
Flattened dependency tree of HOL-Analysis
|
file |
diff |
annotate
|
| Fri, 29 Nov 2019 15:06:04 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Mon, 04 Nov 2019 19:53:43 -0500 |
immler |
Line_Segment is independent of Convex_Euclidean_Space
|
file |
diff |
annotate
|
| Sun, 27 Oct 2019 21:38:41 -0400 |
immler |
some applications of "metric"
|
file |
diff |
annotate
|
| Sun, 27 Oct 2019 16:32:01 +0100 |
immler |
decision procedure for metric spaces, implemented by Maximilian Schäffeler
|
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
|
| Thu, 19 Sep 2019 12:36:15 +0100 |
paulson |
A few more simple results
|
file |
diff |
annotate
|
| Wed, 18 Sep 2019 14:41:37 +0100 |
paulson |
imported new material mostly due to Sébastien Gouëzel
|
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, 19 Mar 2019 16:14:51 +0000 |
paulson |
new material about topology, etc.; also fixes for yesterday's
|
file |
diff |
annotate
|
| Mon, 18 Mar 2019 15:35:34 +0000 |
paulson |
new material;' strengthened material; moved proofs out of Function_Topology in order to lessen its dependencies
|
file |
diff |
annotate
|
| Tue, 22 Jan 2019 12:00:16 +0000 |
paulson |
renamings and new material
|
file |
diff |
annotate
|
| Wed, 16 Jan 2019 19:34:48 -0500 |
immler |
chapters for analysis manual
|
file |
diff |
annotate
|
| Mon, 07 Jan 2019 18:50:41 +0100 |
immler |
moved generalized lemmas
|
file |
diff |
annotate
|
| Mon, 07 Jan 2019 18:42:49 +0100 |
immler |
generalized
|
file |
diff |
annotate
|
| Mon, 07 Jan 2019 13:33:29 +0100 |
immler |
moved setdist to more appropriate places
|
file |
diff |
annotate
|
| Mon, 07 Jan 2019 13:08:50 +0100 |
immler |
split off theory combining Elementary_Topology and Abstract_Topology
|
file |
diff |
annotate
|
| Mon, 07 Jan 2019 12:31:08 +0100 |
immler |
moved material from Connected.thy to more appropriate places
|
file |
diff |
annotate
|
| Mon, 07 Jan 2019 11:29:34 +0100 |
immler |
moved material from Connected.thy to more appropriate places
|
file |
diff |
annotate
|
| Sun, 06 Jan 2019 17:54:49 +0100 |
immler |
moved some material from Connected.thy to more appropriate places
|
file |
diff |
annotate
|
| Sat, 29 Dec 2018 20:32:09 +0100 |
immler |
split off theorems involving classes below metric_space and real_normed_vector
|
file |
diff |
annotate
|