| changeset 63092 | a949b2a5f51d |
| parent 62789 | ce15dd971965 |
| child 63099 | af0e964aad7b |
--- a/src/HOL/Set_Interval.thy Fri May 13 20:22:02 2016 +0200 +++ b/src/HOL/Set_Interval.thy Fri May 13 20:24:10 2016 +0200 @@ -625,7 +625,7 @@ by (auto simp: min_def) lemma Ioc_disjoint: "{a<..b} \<inter> {c<..d} = {} \<longleftrightarrow> b \<le> a \<or> d \<le> c \<or> b \<le> c \<or> d \<le> a" - using assms by auto + by auto end