# HG changeset patch
# User hoelzl
# Date 1354886937 -3600
# Node ID f18b92f91818acfdaa4dc5dfc60c984f587d443c
# Parent  bf01be7d1a44c97710950214fa4b3a3c81b07ea9
add Int_atMost

diff -r bf01be7d1a44 -r f18b92f91818 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Thu Dec 06 23:07:10 2012 +0100
+++ b/src/HOL/Set_Interval.thy	Fri Dec 07 14:28:57 2012 +0100
@@ -351,6 +351,9 @@
 lemma Int_greaterThanLessThan[simp]: "{a<..<b} Int {c<..<d} = {max a c <..< min b d}"
 by auto
 
+lemma Int_atMost[simp]: "{..a} \<inter> {..b} = {.. min a b}"
+  by (auto simp: min_def)
+
 end