diff -r 066bb557570f -r 7619080e49f0 src/HOL/SetInterval.thy
--- 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)