| Tue, 16 Jan 2018 09:30:00 +0100 |
wenzelm |
standardized towards new-style formal comments: isabelle update_comments;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Thu, 21 Dec 2017 21:01:47 +0100 |
nipkow |
tuned op's
|
file |
diff |
annotate
|
| Thu, 21 Dec 2017 20:15:04 +0100 |
nipkow |
tuned op's
|
file |
diff |
annotate
|
| Thu, 21 Dec 2017 19:09:18 +0100 |
nipkow |
tuned op's
|
file |
diff |
annotate
|
| Tue, 31 Oct 2017 13:59:19 +0000 |
paulson |
A few more topological results. And made some slow proofs faster
|
file |
diff |
annotate
|
| Mon, 30 Oct 2017 16:02:59 +0000 |
paulson |
New results in topology, mostly from HOL Light's moretop.ml
|
file |
diff |
annotate
|
| Thu, 19 Oct 2017 17:16:01 +0100 |
paulson |
Switching to inverse image and constant_on, plus some new material
|
file |
diff |
annotate
|
| Tue, 10 Oct 2017 17:15:37 +0100 |
paulson |
Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems
|
file |
diff |
annotate
|
| Tue, 10 Oct 2017 14:03:51 +0100 |
paulson |
Session HOL-Analysis: Moebius functions and the Riemann mapping theorem.
|
file |
diff |
annotate
|
| Mon, 09 Oct 2017 15:34:23 +0100 |
paulson |
new material about connectedness, etc.
|
file |
diff |
annotate
|
| Sun, 20 Aug 2017 03:35:20 +0200 |
Manuel Eberl |
Various lemmas for HOL-Analysis
|
file |
diff |
annotate
|
| Thu, 17 Aug 2017 14:52:56 +0200 |
eberlm |
Replaced subseq with strict_mono
|
file |
diff |
annotate
|
| Wed, 22 Feb 2017 12:30:28 +0000 |
paulson |
new lemmas about segments, etc. Also recast some theorems to use Union rather than general set comprehensions
|
file |
diff |
annotate
|
| Tue, 17 Jan 2017 13:59:10 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Thu, 05 Jan 2017 16:03:23 +0000 |
paulson |
New theory of arcwise connected sets and other new material
|
file |
diff |
annotate
|
| Thu, 05 Jan 2017 14:18:24 +0000 |
paulson |
New material about path connectedness, etc.
|
file |
diff |
annotate
|
| Tue, 25 Oct 2016 15:46:07 +0100 |
paulson |
more new material
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
| Mon, 10 Oct 2016 15:45:41 +0100 |
paulson |
invariance of domain
|
file |
diff |
annotate
|
| Mon, 03 Oct 2016 13:01:01 +0100 |
paulson |
new theorems including the theory FurtherTopology
|
file |
diff |
annotate
|
| Sat, 01 Oct 2016 15:21:43 +0200 |
Lars Hupel |
repair LaTeX
|
file |
diff |
annotate
|
| Fri, 30 Sep 2016 15:51:43 +0200 |
hoelzl |
HOL-Analysis: fix latex generation
|
file |
diff |
annotate
|
| Fri, 30 Sep 2016 15:35:32 +0200 |
hoelzl |
HOL-Analysis: move Continuum_Not_Denumerable from Library
|
file |
diff |
annotate
|
| Fri, 30 Sep 2016 14:05:51 +0100 |
paulson |
new material on paths, etc. Also rationalisation
|
file |
diff |
annotate
|
| Thu, 29 Sep 2016 12:58:55 +0100 |
paulson |
more new material
|
file |
diff |
annotate
|
| Wed, 21 Sep 2016 16:59:51 +0100 |
paulson |
new material about topological concepts, etc
|
file |
diff |
annotate
|
| Thu, 15 Sep 2016 15:48:37 +0100 |
paulson |
lots of new results about topology, affine dimension etc
|
file |
diff |
annotate
|
| Mon, 08 Aug 2016 14:13:14 +0200 |
hoelzl |
rename HOL-Multivariate_Analysis to HOL-Analysis.
|
file |
diff |
annotate
| base
|