# HG changeset patch
# User hoelzl
# Date 1377612387 -7200
# Node ID ad2e09c30aa83ffa00e773abfd5b18815eb2581f
# Parent  5e47c31c6f7c391a10e4a4df700e68ba7b0917d7
renamed inner_dense_linorder to dense_linorder

diff -r 5e47c31c6f7c -r ad2e09c30aa8 src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Tue Aug 27 14:37:56 2013 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Tue Aug 27 16:06:27 2013 +0200
@@ -246,7 +246,7 @@
 
 end
 
-class linear_continuum = conditionally_complete_linorder + inner_dense_linorder +
+class linear_continuum = conditionally_complete_linorder + dense_linorder +
   assumes UNIV_not_singleton: "\<exists>a b::'a. a \<noteq> b"
 begin
 
diff -r 5e47c31c6f7c -r ad2e09c30aa8 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Tue Aug 27 14:37:56 2013 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Tue Aug 27 16:06:27 2013 +0200
@@ -293,7 +293,7 @@
 lemma ereal_dense2: "x < y \<Longrightarrow> \<exists>z. x < ereal z \<and> ereal z < y"
   using lt_ex gt_ex dense by (cases x y rule: ereal2_cases) auto
 
-instance ereal :: inner_dense_linorder
+instance ereal :: dense_linorder
   by default (blast dest: ereal_dense2)
 
 instance ereal :: ordered_ab_semigroup_add
diff -r 5e47c31c6f7c -r ad2e09c30aa8 src/HOL/Library/Liminf_Limsup.thy
--- a/src/HOL/Library/Liminf_Limsup.thy	Tue Aug 27 14:37:56 2013 +0200
+++ b/src/HOL/Library/Liminf_Limsup.thy	Tue Aug 27 16:06:27 2013 +0200
@@ -9,13 +9,13 @@
 begin
 
 lemma le_Sup_iff_less:
-  fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
+  fixes x :: "'a :: {complete_linorder, dense_linorder}"
   shows "x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs")
   unfolding le_SUP_iff
   by (blast intro: less_imp_le less_trans less_le_trans dest: dense)
 
 lemma Inf_le_iff_less:
-  fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
+  fixes x :: "'a :: {complete_linorder, dense_linorder}"
   shows "(INF i:A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
   unfolding INF_le_iff
   by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
diff -r 5e47c31c6f7c -r ad2e09c30aa8 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Tue Aug 27 14:37:56 2013 +0200
+++ b/src/HOL/Orderings.thy	Tue Aug 27 16:06:27 2013 +0200
@@ -1230,10 +1230,10 @@
 
 subsection {* Dense orders *}
 
-class inner_dense_order = order +
+class dense_order = order +
   assumes dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
 
-class inner_dense_linorder = linorder + inner_dense_order
+class dense_linorder = linorder + dense_order
 begin
 
 lemma dense_le:
@@ -1312,7 +1312,7 @@
 class no_bot = order + 
   assumes lt_ex: "\<exists>y. y < x"
 
-class unbounded_dense_linorder = inner_dense_linorder + no_top + no_bot
+class unbounded_dense_linorder = dense_linorder + no_top + no_bot
 
 
 subsection {* Wellorders *}
diff -r 5e47c31c6f7c -r ad2e09c30aa8 src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Tue Aug 27 14:37:56 2013 +0200
+++ b/src/HOL/Probability/Borel_Space.thy	Tue Aug 27 16:06:27 2013 +0200
@@ -251,7 +251,7 @@
   by (blast intro: borel_open borel_closed)+
 
 lemma open_Collect_less:
-  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {inner_dense_linorder, linorder_topology}"
+  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {dense_linorder, linorder_topology}"
   assumes "continuous_on UNIV f"
   assumes "continuous_on UNIV g"
   shows "open {x. f x < g x}"
@@ -264,14 +264,14 @@
 qed
 
 lemma closed_Collect_le:
-  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {inner_dense_linorder, linorder_topology}"
+  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {dense_linorder, linorder_topology}"
   assumes f: "continuous_on UNIV f"
   assumes g: "continuous_on UNIV g"
   shows "closed {x. f x \<le> g x}"
   using open_Collect_less[OF g f] unfolding not_less[symmetric] Collect_neg_eq open_closed .
 
 lemma borel_measurable_less[measurable]:
-  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}"
+  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology}"
   assumes "f \<in> borel_measurable M"
   assumes "g \<in> borel_measurable M"
   shows "{w \<in> space M. f w < g w} \<in> sets M"
@@ -285,7 +285,7 @@
 qed
 
 lemma
-  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}"
+  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology}"
   assumes f[measurable]: "f \<in> borel_measurable M"
   assumes g[measurable]: "g \<in> borel_measurable M"
   shows borel_measurable_le[measurable]: "{w \<in> space M. f w \<le> g w} \<in> sets M"
@@ -755,11 +755,11 @@
   by (simp add: field_divide_inverse)
 
 lemma borel_measurable_max[measurable (raw)]:
-  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. max (g x) (f x) :: 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}) \<in> borel_measurable M"
+  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. max (g x) (f x) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M"
   by (simp add: max_def)
 
 lemma borel_measurable_min[measurable (raw)]:
-  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. min (g x) (f x) :: 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}) \<in> borel_measurable M"
+  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. min (g x) (f x) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M"
   by (simp add: min_def)
 
 lemma borel_measurable_abs[measurable (raw)]:
diff -r 5e47c31c6f7c -r ad2e09c30aa8 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Tue Aug 27 14:37:56 2013 +0200
+++ b/src/HOL/Set_Interval.thy	Tue Aug 27 16:06:27 2013 +0200
@@ -373,7 +373,7 @@
 end
 
 
-context inner_dense_linorder
+context dense_linorder
 begin
 
 lemma greaterThanLessThan_empty_iff[simp]:
@@ -519,7 +519,7 @@
 end
 
 lemma
-  fixes x y :: "'a :: {complete_lattice, inner_dense_linorder}"
+  fixes x y :: "'a :: {complete_lattice, dense_linorder}"
   shows Sup_lessThan[simp]: "Sup {..< y} = y"
     and Sup_atLeastLessThan[simp]: "x < y \<Longrightarrow> Sup { x ..< y} = y"
     and Sup_greaterThanLessThan[simp]: "x < y \<Longrightarrow> Sup { x <..< y} = y"