--- a/src/HOL/Set_Interval.thy Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Set_Interval.thy Fri Oct 18 10:43:20 2013 +0200
@@ -180,19 +180,19 @@
context ord
begin
-lemma greaterThanLessThan_iff [simp,no_atp]:
+lemma greaterThanLessThan_iff [simp]:
"(i : {l<..<u}) = (l < i & i < u)"
by (simp add: greaterThanLessThan_def)
-lemma atLeastLessThan_iff [simp,no_atp]:
+lemma atLeastLessThan_iff [simp]:
"(i : {l..<u}) = (l <= i & i < u)"
by (simp add: atLeastLessThan_def)
-lemma greaterThanAtMost_iff [simp,no_atp]:
+lemma greaterThanAtMost_iff [simp]:
"(i : {l<..u}) = (l < i & i <= u)"
by (simp add: greaterThanAtMost_def)
-lemma atLeastAtMost_iff [simp,no_atp]:
+lemma atLeastAtMost_iff [simp]:
"(i : {l..u}) = (l <= i & i <= u)"
by (simp add: atLeastAtMost_def)
@@ -1196,7 +1196,7 @@
subsubsection {* Some Subset Conditions *}
-lemma ivl_subset [simp,no_atp]:
+lemma ivl_subset [simp]:
"({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)