| 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 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 |
| Thu, 17 Jan 2013 11:57:17 +0100 | hoelzl | generalize compact_path_image to topological_space | file | diff | annotate |
| Mon, 14 Jan 2013 18:30:36 +0100 | hoelzl | differentiate (cover) compactness and sequential compactness | file | diff | annotate |
| Fri, 14 Dec 2012 15:46:01 +0100 | hoelzl | Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors | file | diff | annotate |
| Fri, 28 Sep 2012 23:45:15 +0200 | wenzelm | tuned proofs; | file | diff | annotate |
| Fri, 28 Sep 2012 23:40:48 +0200 | wenzelm | tuned proofs; | file | diff | annotate |