src/HOL/SetInterval.thy
changeset 35828 46cfc4b8112e
parent 35644 d20cf282342e
child 36307 1732232f9b27
     1.1 --- a/src/HOL/SetInterval.thy	Wed Mar 17 19:37:44 2010 +0100
     1.2 +++ b/src/HOL/SetInterval.thy	Thu Mar 18 12:58:52 2010 +0100
     1.3 @@ -165,19 +165,19 @@
     1.4  context ord
     1.5  begin
     1.6  
     1.7 -lemma greaterThanLessThan_iff [simp,noatp]:
     1.8 +lemma greaterThanLessThan_iff [simp,no_atp]:
     1.9    "(i : {l<..<u}) = (l < i & i < u)"
    1.10  by (simp add: greaterThanLessThan_def)
    1.11  
    1.12 -lemma atLeastLessThan_iff [simp,noatp]:
    1.13 +lemma atLeastLessThan_iff [simp,no_atp]:
    1.14    "(i : {l..<u}) = (l <= i & i < u)"
    1.15  by (simp add: atLeastLessThan_def)
    1.16  
    1.17 -lemma greaterThanAtMost_iff [simp,noatp]:
    1.18 +lemma greaterThanAtMost_iff [simp,no_atp]:
    1.19    "(i : {l<..u}) = (l < i & i <= u)"
    1.20  by (simp add: greaterThanAtMost_def)
    1.21  
    1.22 -lemma atLeastAtMost_iff [simp,noatp]:
    1.23 +lemma atLeastAtMost_iff [simp,no_atp]:
    1.24    "(i : {l..u}) = (l <= i & i <= u)"
    1.25  by (simp add: atLeastAtMost_def)
    1.26  
    1.27 @@ -844,7 +844,7 @@
    1.28  
    1.29  subsubsection {* Some Subset Conditions *}
    1.30  
    1.31 -lemma ivl_subset [simp,noatp]:
    1.32 +lemma ivl_subset [simp,no_atp]:
    1.33   "({i..<j} \<subseteq> {m..<n}) = (j \<le> i | m \<le> i & j \<le> (n::'a::linorder))"
    1.34  apply(auto simp:linorder_not_le)
    1.35  apply(rule ccontr)