# HG changeset patch
# User hoelzl
# Date 1366878956 -7200
# Node ID 916271d524668c2eed3ab83441b4629c0d444c7c
# Parent  9328c6681f3cbdbf652b3e7198f7215a8ec09a42
renamed linear_continuum_topology to connected_linorder_topology (and mention in NEWS)

diff -r 9328c6681f3c -r 916271d52466 NEWS
--- a/NEWS	Wed Apr 24 13:28:30 2013 +0200
+++ b/NEWS	Thu Apr 25 10:35:56 2013 +0200
@@ -133,7 +133,8 @@
 
  - connected from Multivariate_Analysis. Use it to prove the
    intermediate value theorem. Show connectedness of intervals on order
-   topologies which are a inner dense, conditionally-complete linorder.
+   topologies which are a inner dense, conditionally-complete linorder
+   (named connected_linorder_topology).
 
  - first_countable_topology from Multivariate_Analysis. Is used to
    show equivalence of properties on the neighbourhood filter of x and on
diff -r 9328c6681f3c -r 916271d52466 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Wed Apr 24 13:28:30 2013 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Thu Apr 25 10:35:56 2013 +0200
@@ -1572,7 +1572,7 @@
 
 subsubsection "Topological space"
 
-instantiation ereal :: linorder_topology
+instantiation ereal :: connected_linorder_topology
 begin
 
 definition "open_ereal" :: "ereal set \<Rightarrow> bool" where
diff -r 9328c6681f3c -r 916271d52466 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Wed Apr 24 13:28:30 2013 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Thu Apr 25 10:35:56 2013 +0200
@@ -860,7 +860,7 @@
   qed
 qed
 
-instance real :: linear_continuum_topology ..
+instance real :: connected_linorder_topology ..
 
 lemmas open_real_greaterThan = open_greaterThan[where 'a=real]
 lemmas open_real_lessThan = open_lessThan[where 'a=real]
diff -r 9328c6681f3c -r 916271d52466 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Wed Apr 24 13:28:30 2013 +0200
+++ b/src/HOL/Topological_Spaces.thy	Thu Apr 25 10:35:56 2013 +0200
@@ -2079,7 +2079,7 @@
 
 section {* Connectedness *}
 
-class linear_continuum_topology = linorder_topology + conditionally_complete_linorder + inner_dense_linorder
+class connected_linorder_topology = linorder_topology + conditionally_complete_linorder + inner_dense_linorder
 begin
 
 lemma Inf_notin_open:
@@ -2111,7 +2111,7 @@
 end
 
 lemma connectedI_interval:
-  fixes U :: "'a :: linear_continuum_topology set"
+  fixes U :: "'a :: connected_linorder_topology set"
   assumes *: "\<And>x y z. x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x \<le> z \<Longrightarrow> z \<le> y \<Longrightarrow> z \<in> U"
   shows "connected U"
 proof (rule connectedI)
@@ -2154,35 +2154,35 @@
 qed
 
 lemma connected_iff_interval:
-  fixes U :: "'a :: linear_continuum_topology set"
+  fixes U :: "'a :: connected_linorder_topology set"
   shows "connected U \<longleftrightarrow> (\<forall>x\<in>U. \<forall>y\<in>U. \<forall>z. x \<le> z \<longrightarrow> z \<le> y \<longrightarrow> z \<in> U)"
   by (auto intro: connectedI_interval dest: connectedD_interval)
 
-lemma connected_UNIV[simp]: "connected (UNIV::'a::linear_continuum_topology set)"
+lemma connected_UNIV[simp]: "connected (UNIV::'a::connected_linorder_topology set)"
   unfolding connected_iff_interval by auto
 
-lemma connected_Ioi[simp]: "connected {a::'a::linear_continuum_topology <..}"
+lemma connected_Ioi[simp]: "connected {a::'a::connected_linorder_topology <..}"
   unfolding connected_iff_interval by auto
 
-lemma connected_Ici[simp]: "connected {a::'a::linear_continuum_topology ..}"
+lemma connected_Ici[simp]: "connected {a::'a::connected_linorder_topology ..}"
   unfolding connected_iff_interval by auto
 
-lemma connected_Iio[simp]: "connected {..< a::'a::linear_continuum_topology}"
+lemma connected_Iio[simp]: "connected {..< a::'a::connected_linorder_topology}"
   unfolding connected_iff_interval by auto
 
-lemma connected_Iic[simp]: "connected {.. a::'a::linear_continuum_topology}"
+lemma connected_Iic[simp]: "connected {.. a::'a::connected_linorder_topology}"
   unfolding connected_iff_interval by auto
 
-lemma connected_Ioo[simp]: "connected {a <..< b::'a::linear_continuum_topology}"
+lemma connected_Ioo[simp]: "connected {a <..< b::'a::connected_linorder_topology}"
   unfolding connected_iff_interval by auto
 
-lemma connected_Ioc[simp]: "connected {a <.. b::'a::linear_continuum_topology}"
+lemma connected_Ioc[simp]: "connected {a <.. b::'a::connected_linorder_topology}"
   unfolding connected_iff_interval by auto
 
-lemma connected_Ico[simp]: "connected {a ..< b::'a::linear_continuum_topology}"
+lemma connected_Ico[simp]: "connected {a ..< b::'a::connected_linorder_topology}"
   unfolding connected_iff_interval by auto
 
-lemma connected_Icc[simp]: "connected {a .. b::'a::linear_continuum_topology}"
+lemma connected_Icc[simp]: "connected {a .. b::'a::connected_linorder_topology}"
   unfolding connected_iff_interval by auto
 
 lemma connected_contains_Ioo: 
@@ -2193,7 +2193,7 @@
 subsection {* Intermediate Value Theorem *}
 
 lemma IVT':
-  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
+  fixes f :: "'a :: connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
   assumes y: "f a \<le> y" "y \<le> f b" "a \<le> b"
   assumes *: "continuous_on {a .. b} f"
   shows "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
@@ -2206,7 +2206,7 @@
 qed
 
 lemma IVT2':
-  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
+  fixes f :: "'a :: connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
   assumes y: "f b \<le> y" "y \<le> f a" "a \<le> b"
   assumes *: "continuous_on {a .. b} f"
   shows "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
@@ -2219,17 +2219,17 @@
 qed
 
 lemma IVT:
-  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
+  fixes f :: "'a :: connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
   shows "f a \<le> y \<Longrightarrow> y \<le> f b \<Longrightarrow> a \<le> b \<Longrightarrow> (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x) \<Longrightarrow> \<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
   by (rule IVT') (auto intro: continuous_at_imp_continuous_on)
 
 lemma IVT2:
-  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
+  fixes f :: "'a :: connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
   shows "f b \<le> y \<Longrightarrow> y \<le> f a \<Longrightarrow> a \<le> b \<Longrightarrow> (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x) \<Longrightarrow> \<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
   by (rule IVT2') (auto intro: continuous_at_imp_continuous_on)
 
 lemma continuous_inj_imp_mono:
-  fixes f :: "'a::linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
+  fixes f :: "'a::connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
   assumes x: "a < x" "x < b"
   assumes cont: "continuous_on {a..b} f"
   assumes inj: "inj_on f {a..b}"