--- 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"