# HG changeset patch
# User huffman
# Date 1272337381 25200
# Node ID a65320184de97350e1df69993e3e6bfdb0981f38
# Parent  d8b26fac82f5281b2f5e537045694c93398e220d
move intervals section heading

diff -r d8b26fac82f5 -r a65320184de9 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Apr 26 19:58:51 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Apr 26 20:03:01 2010 -0700
@@ -4697,7 +4697,7 @@
     by (auto simp add: dist_commute)
 qed
 
-(* A cute way of denoting open and closed intervals using overloading.       *)
+subsection {* Intervals *}
 
 lemma interval: fixes a :: "'a::ord^'n" shows
   "{a <..< b} = {x::'a^'n. \<forall>i. a$i < x$i \<and> x$i < b$i}" and
@@ -5108,7 +5108,7 @@
   thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
 qed
 
-subsection {* Intervals *}
+text {* Intervals in general, including infinite and mixtures of open and closed. *}
 
 definition "is_interval s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i. ((a$i \<le> x$i \<and> x$i \<le> b$i) \<or> (b$i \<le> x$i \<and> x$i \<le> a$i)))  \<longrightarrow> x \<in> s)"