1.1 --- a/src/HOL/Set_Interval.thy	Thu Dec 06 23:07:10 2012 +0100
     1.2 +++ b/src/HOL/Set_Interval.thy	Fri Dec 07 14:28:57 2012 +0100
     1.3 @@ -351,6 +351,9 @@
     1.4  lemma Int_greaterThanLessThan[simp]: "{a<..<b} Int {c<..<d} = {max a c <..< min b d}"
     1.5  by auto
     1.6  
     1.7 +lemma Int_atMost[simp]: "{..a} \<inter> {..b} = {.. min a b}"
     1.8 +  by (auto simp: min_def)
     1.9 +
    1.10  end
    1.11  
    1.12