Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/Dedekind_Real.thy
changeset 53215 5e47c31c6f7c
parent 49962 a8cc904a6820
child 53373 3ca9e79ac926 
--- a/src/HOL/ex/Dedekind_Real.thy	Mon Aug 26 23:39:53 2013 +0200
+++ b/src/HOL/ex/Dedekind_Real.thy	Tue Aug 27 14:37:56 2013 +0200
@@ -24,7 +24,7 @@
             (\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u))))"
 
 lemma interval_empty_iff:
-  "{y. (x::'a::dense_linorder) < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
+  "{y. (x::'a::unbounded_dense_linorder) < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
   by (auto dest: dense)
isabelle