1.1 --- a/src/HOL/Library/Convex_Euclidean_Space.thy	Tue Jun 02 10:00:29 2009 +0200
     1.2 +++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Tue Jun 02 10:02:08 2009 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4 -(* Title:      Convex
     1.5 -   ID:         $Id: 
     1.6 -   Author:     Robert Himmelmann, TU Muenchen*)
     1.7 +(*  Title:      HOL/Library/Convex_Euclidean_Space.thy
     1.8 +    Author:     Robert Himmelmann, TU Muenchen
     1.9 +*)
    1.10  
    1.11  header {* Convex sets, functions and related things. *}
    1.12  
    1.13 @@ -2192,7 +2192,7 @@
    1.14  lemma convex_interval: "convex {a .. b}" "convex {a<..<b::real^'n::finite}"
    1.15    apply(rule_tac[!] is_interval_convex) using is_interval_interval by auto
    1.16  
    1.17 -subsection {* On real^1, is_interval, convex and connected are all equivalent. *}
    1.18 +subsection {* On @{text "real^1"}, @{text "is_interval"}, @{text "convex"} and @{text "connected"} are all equivalent. *}
    1.19  
    1.20  lemma is_interval_1:
    1.21    "is_interval s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b \<longrightarrow> x \<in> s)"