src/HOL/SetInterval.thy
changeset 29709 cf8476cc440d
parent 29667 53103fc8ffa3
child 29920 b95f5b8b93dd
     1.1 --- a/src/HOL/SetInterval.thy	Mon Feb 02 13:56:22 2009 +0100
     1.2 +++ b/src/HOL/SetInterval.thy	Mon Feb 02 13:56:23 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/SetInterval.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Tobias Nipkow and Clemens Ballarin
     1.7                  Additions by Jeremy Avigad in March 2004
     1.8      Copyright   2000  TU Muenchen
     1.9 @@ -138,7 +137,7 @@
    1.10       "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))"
    1.11  apply (rule iffI)
    1.12   apply (erule equalityE)
    1.13 - apply (simp_all add: greaterThan_subset_iff)
    1.14 + apply simp_all
    1.15  done
    1.16  
    1.17  lemma atMost_subset_iff [iff]: "(atMost x \<subseteq> atMost y) = (x \<le> (y::'a::order))"
    1.18 @@ -157,7 +156,7 @@
    1.19       "(lessThan x = lessThan y) = (x = (y::'a::linorder))"
    1.20  apply (rule iffI)
    1.21   apply (erule equalityE)
    1.22 - apply (simp_all add: lessThan_subset_iff)
    1.23 + apply simp_all
    1.24  done
    1.25  
    1.26  
    1.27 @@ -201,7 +200,7 @@
    1.28  lemma greaterThanAtMost_empty[simp]:"l \<le> k ==> {k<..l} = {}"
    1.29  by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)
    1.30  
    1.31 -lemma greaterThanLessThan_empty[simp]:"l \<le> k ==> {k<..l} = {}"
    1.32 +lemma greaterThanLessThan_empty[simp]:"l \<le> k ==> {k<..<l} = {}"
    1.33  by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def)
    1.34  
    1.35  lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}"