| Thu, 04 Aug 2016 18:45:28 +0200 |
hoelzl |
HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
|
file |
diff |
annotate
|
| Fri, 29 Jul 2016 20:34:07 +0200 |
wenzelm |
more accurate cong del;
|
file |
diff |
annotate
|
| Thu, 14 Jul 2016 14:48:49 +0100 |
paulson |
More advanced theorems about retracts, homotopies., etc
|
file |
diff |
annotate
|
| Wed, 13 Jul 2016 17:14:17 +0100 |
paulson |
lots of new theorems about differentiable_on, retracts, ANRs, etc.
|
file |
diff |
annotate
|
| Wed, 15 Jun 2016 22:19:03 +0200 |
hoelzl |
move open_Collect_eq/less to HOL
|
file |
diff |
annotate
|
| Wed, 15 Jun 2016 15:52:24 +0100 |
paulson |
Urysohn's lemma, Dugundji extension theorem and many other proofs
|
file |
diff |
annotate
|
| Tue, 14 Jun 2016 15:34:21 +0100 |
paulson |
new results about topology
|
file |
diff |
annotate
|
| Fri, 27 May 2016 20:23:55 +0200 |
wenzelm |
tuned proofs, to allow unfold_abs_def;
|
file |
diff |
annotate
|
| Wed, 25 May 2016 16:01:42 +0200 |
wenzelm |
updated 'define';
|
file |
diff |
annotate
|
| Tue, 24 May 2016 15:08:07 +0100 |
paulson |
Merge
|
file |
diff |
annotate
|
| Tue, 24 May 2016 13:57:34 +0100 |
paulson |
renamings and new material
|
file |
diff |
annotate
|
| Mon, 23 May 2016 15:33:24 +0100 |
paulson |
Lots of new material for multivariate analysis
|
file |
diff |
annotate
|
| Fri, 13 May 2016 20:24:10 +0200 |
wenzelm |
eliminated use of empty "assms";
|
file |
diff |
annotate
|
| Tue, 10 May 2016 11:56:23 +0100 |
paulson |
two new lemmas about segments
|
file |
diff |
annotate
|
| Mon, 09 May 2016 17:23:19 +0100 |
paulson |
lemmas about dimension, hyperplanes, span, etc.
|
file |
diff |
annotate
|
| Mon, 09 May 2016 16:02:23 +0100 |
paulson |
renamings and refinements
|
file |
diff |
annotate
|
| Mon, 25 Apr 2016 16:09:26 +0200 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
| Mon, 18 Apr 2016 16:50:19 +0100 |
paulson |
tidying some proofs; getting rid of "nonempty_witness"
|
file |
diff |
annotate
|
| Mon, 18 Apr 2016 15:40:55 +0100 |
paulson |
numerous theorems about affine hulls, hyperplanes, etc.
|
file |
diff |
annotate
|
| Mon, 18 Apr 2016 14:30:32 +0100 |
paulson |
new theorems about convex hulls, etc.; also, renamed some theorems
|
file |
diff |
annotate
|
| Tue, 12 Apr 2016 11:18:29 +0200 |
immler |
generalized
|
file |
diff |
annotate
|
| Mon, 11 Apr 2016 16:27:42 +0100 |
paulson |
lots of new theorems for multivariate analysis
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 16:52:56 +0100 |
paulson |
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
|
file |
diff |
annotate
|
| Wed, 16 Mar 2016 13:57:06 +0000 |
paulson |
Contractible sets. Also removal of obsolete theorems and refactoring
|
file |
diff |
annotate
|
| Mon, 14 Mar 2016 15:58:02 +0000 |
paulson |
New results about paths, segments, etc. The notion of simply_connected.
|
file |
diff |
annotate
|
| Mon, 14 Mar 2016 14:19:06 +0000 |
paulson |
Refactoring (moving theorems into better locations), plus a bit of new material
|
file |
diff |
annotate
|
| Mon, 07 Mar 2016 14:34:45 +0000 |
paulson |
new material to Blochj's theorem, as well as supporting lemmas
|
file |
diff |
annotate
|
| Wed, 24 Feb 2016 16:00:57 +0000 |
paulson |
Merge
|
file |
diff |
annotate
|
| Wed, 24 Feb 2016 15:51:01 +0000 |
paulson |
Substantial new material for multivariate analysis. Also removal of some duplicates.
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 18:04:31 +0100 |
nipkow |
resolved conflict
|
file |
diff |
annotate
|