summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Multivariate_Analysis/Path_Connected.thy

changeset 58877 | 262572d90bc6 |

parent 56371 | fb9ae0727548 |

child 59557 | ebd8ecacfba6 |

1.1 --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Sun Nov 02 17:06:05 2014 +0100 1.2 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Sun Nov 02 17:09:04 2014 +0100 1.3 @@ -2,7 +2,7 @@ 1.4 Author: Robert Himmelmann, TU Muenchen 1.5 *) 1.6 1.7 -header {* Continuous paths and path-connected sets *} 1.8 +section {* Continuous paths and path-connected sets *} 1.9 1.10 theory Path_Connected 1.11 imports Convex_Euclidean_Space