| Thu, 30 May 2013 23:29:33 +0200 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Thu, 25 Apr 2013 11:59:21 +0200 |
hoelzl |
revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
|
file |
diff |
annotate
|
| Thu, 25 Apr 2013 10:35:56 +0200 |
hoelzl |
renamed linear_continuum_topology to connected_linorder_topology (and mention in NEWS)
|
file |
diff |
annotate
|
| Wed, 24 Apr 2013 13:28:30 +0200 |
hoelzl |
spell conditional_ly_-complete lattices correct
|
file |
diff |
annotate
|
| Tue, 09 Apr 2013 14:04:41 +0200 |
hoelzl |
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 12:20:52 +0100 |
hoelzl |
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
move connected to HOL image; used to show intermediate value theorem
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
move first_countable_topology to the HOL image
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:42 +0100 |
hoelzl |
move topological_space to its own theory
|
file |
diff |
annotate
|