--- a/src/HOL/SetInterval.thy Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/SetInterval.thy Tue Sep 07 10:05:19 2010 +0200
@@ -241,7 +241,7 @@
lemma atLeastatMost_psubset_iff:
"{a..b} < {c..d} \<longleftrightarrow>
((~ a <= b) | c <= a & b <= d & (c < a | b < d)) & c <= d"
-by(simp add: psubset_eq expand_set_eq less_le_not_le)(blast intro: order_trans)
+by(simp add: psubset_eq set_ext_iff less_le_not_le)(blast intro: order_trans)
lemma atLeastAtMost_singleton_iff[simp]:
"{a .. b} = {c} \<longleftrightarrow> a = b \<and> b = c"