| Wed, 02 May 2018 13:49:38 +0200 |
immler |
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
|
file |
diff |
annotate
|
| Mon, 09 Apr 2018 16:20:23 +0200 |
nipkow |
removed dots at the end of (sub)titles
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
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 17:20:56 +0000 |
paulson |
More topological results overlooked last time
|
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, 28 Feb 2017 13:51:47 +0000 |
paulson |
Renamed ii to imaginary_unit in order to free up ii as a variable name. Also replaced some legacy def commands
|
file |
diff |
annotate
|
| Tue, 21 Feb 2017 17:12:10 +0000 |
paulson |
some new material, also recasting some theorems using “obtains”
|
file |
diff |
annotate
|
| Tue, 17 Jan 2017 13:59:10 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Mon, 09 Jan 2017 15:54:48 +0000 |
paulson |
fixed LaTeX problems
|
file |
diff |
annotate
|
| Mon, 09 Jan 2017 14:40:31 +0000 |
paulson |
Jordan Curve Theorem
|
file |
diff |
annotate
|
| Mon, 09 Jan 2017 14:00:13 +0000 |
paulson |
Advanced topology
|
file |
diff |
annotate
|
| Thu, 05 Jan 2017 16:37:49 +0000 |
paulson |
facts about ANRs, ENRs, covering spaces
|
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 15:03:37 +0000 |
paulson |
connectedness, circles not simply connected , punctured universe
|
file |
diff |
annotate
|
| Sat, 19 Nov 2016 20:10:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Wed, 26 Oct 2016 12:22:58 +0100 |
paulson |
Deleted spurious markup
|
file |
diff |
annotate
|
| Tue, 25 Oct 2016 16:30:13 +0100 |
paulson |
more new material
|
file |
diff |
annotate
|
| Tue, 25 Oct 2016 15:46:07 +0100 |
paulson |
more new material
|
file |
diff |
annotate
|
| Tue, 18 Oct 2016 19:12:40 +0100 |
paulson |
Inserted necessary dependency
|
file |
diff |
annotate
|
| Tue, 18 Oct 2016 17:29:28 +0200 |
hoelzl |
HOL-Analysis: move Function Topology from AFP/Ergodict_Theory; HOL-Probability: move Essential Supremum from AFP/Lp
|
file |
diff |
annotate
| base
|