--- a/src/HOL/SetInterval.thy Wed Aug 15 09:02:11 2007 +0200
+++ b/src/HOL/SetInterval.thy Wed Aug 15 12:52:56 2007 +0200
@@ -153,19 +153,19 @@
subsection {*Two-sided intervals*}
-lemma greaterThanLessThan_iff [simp]:
+lemma greaterThanLessThan_iff [simp,noatp]:
"(i : {l<..<u}) = (l < i & i < u)"
by (simp add: greaterThanLessThan_def)
-lemma atLeastLessThan_iff [simp]:
+lemma atLeastLessThan_iff [simp,noatp]:
"(i : {l..<u}) = (l <= i & i < u)"
by (simp add: atLeastLessThan_def)
-lemma greaterThanAtMost_iff [simp]:
+lemma greaterThanAtMost_iff [simp,noatp]:
"(i : {l<..u}) = (l < i & i <= u)"
by (simp add: greaterThanAtMost_def)
-lemma atLeastAtMost_iff [simp]:
+lemma atLeastAtMost_iff [simp,noatp]:
"(i : {l..u}) = (l <= i & i <= u)"
by (simp add: atLeastAtMost_def)
@@ -569,7 +569,7 @@
subsubsection {* Some Subset Conditions *}
-lemma ivl_subset[simp]:
+lemma ivl_subset [simp,noatp]:
"({i..<j} \<subseteq> {m..<n}) = (j \<le> i | m \<le> i & j \<le> (n::'a::linorder))"
apply(auto simp:linorder_not_le)
apply(rule ccontr)