# HG changeset patch
# User berghofe
# Date 1243929728 -7200
# Node ID fef52c5c1462fab70b6d9460f6353ea2ae49bece
# Parent  0c4ec2867a4ecd7ff622d606d56f4b5e744008c2
Enclosed parts of subsection in @{text ...} to make LaTeX happy.

diff -r 0c4ec2867a4e -r fef52c5c1462 src/HOL/Library/Convex_Euclidean_Space.thy
--- a/src/HOL/Library/Convex_Euclidean_Space.thy	Tue Jun 02 10:00:29 2009 +0200
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Tue Jun 02 10:02:08 2009 +0200
@@ -1,6 +1,6 @@
-(* Title:      Convex
-   ID:         $Id: 
-   Author:     Robert Himmelmann, TU Muenchen*)
+(*  Title:      HOL/Library/Convex_Euclidean_Space.thy
+    Author:     Robert Himmelmann, TU Muenchen
+*)
 
 header {* Convex sets, functions and related things. *}
 
@@ -2192,7 +2192,7 @@
 lemma convex_interval: "convex {a .. b}" "convex {a<..<b::real^'n::finite}"
   apply(rule_tac[!] is_interval_convex) using is_interval_interval by auto
 
-subsection {* On real^1, is_interval, convex and connected are all equivalent. *}
+subsection {* On @{text "real^1"}, @{text "is_interval"}, @{text "convex"} and @{text "connected"} are all equivalent. *}
 
 lemma is_interval_1:
   "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)"