# HG changeset patch
# User haftmann
# Date 1233579383 -3600
# Node ID cf8476cc440d253e07552ea2be3f64d29c13b6b5
# Parent  e40b70d3890914a490d25c41f0068eb2fcebeeab
fixed proposition slip

diff -r e40b70d38909 -r cf8476cc440d src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Mon Feb 02 13:56:22 2009 +0100
+++ b/src/HOL/SetInterval.thy	Mon Feb 02 13:56:23 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/SetInterval.thy
-    ID:         $Id$
     Author:     Tobias Nipkow and Clemens Ballarin
                 Additions by Jeremy Avigad in March 2004
     Copyright   2000  TU Muenchen
@@ -138,7 +137,7 @@
      "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))"
 apply (rule iffI)
  apply (erule equalityE)
- apply (simp_all add: greaterThan_subset_iff)
+ apply simp_all
 done
 
 lemma atMost_subset_iff [iff]: "(atMost x \<subseteq> atMost y) = (x \<le> (y::'a::order))"
@@ -157,7 +156,7 @@
      "(lessThan x = lessThan y) = (x = (y::'a::linorder))"
 apply (rule iffI)
  apply (erule equalityE)
- apply (simp_all add: lessThan_subset_iff)
+ apply simp_all
 done
 
 
@@ -201,7 +200,7 @@
 lemma greaterThanAtMost_empty[simp]:"l \<le> k ==> {k<..l} = {}"
 by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)
 
-lemma greaterThanLessThan_empty[simp]:"l \<le> k ==> {k<..l} = {}"
+lemma greaterThanLessThan_empty[simp]:"l \<le> k ==> {k<..<l} = {}"
 by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def)
 
 lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}"