# HG changeset patch
# User nipkow
# Date 1580830609 -3600
# Node ID 6a1c1d1ce6ae6aabd719fc74971ca6a82bc5783c
# Parent  63b2789259e7b09789788289746f0b155e5be4dc
tuned

diff -r 63b2789259e7 -r 6a1c1d1ce6ae src/HOL/Data_Structures/Interval_Tree.thy
--- a/src/HOL/Data_Structures/Interval_Tree.thy	Mon Feb 03 18:22:59 2020 +0100
+++ b/src/HOL/Data_Structures/Interval_Tree.thy	Tue Feb 04 16:36:49 2020 +0100
@@ -231,16 +231,14 @@
           case False
           have "\<not>overlap x rp" if asm: "rp \<in> set_tree r" for rp
           proof -
-            have "p \<in> set (inorder l)" using p(1) by (simp)
-            moreover have "rp \<in> set (inorder r)" using asm by (simp)
-            ultimately have "low p \<le> low rp"
-              using Node(4) by(fastforce simp: sorted_wrt_append ivl_less)
+            have "low p \<le> low rp"
+              using asm p(1) Node(4) by(fastforce simp: sorted_wrt_append ivl_less)
             then show ?thesis
               using False by (auto simp: overlap_def)
           qed
           then show ?thesis
             unfolding search_eval search_l
-            using a_disjoint by (fastforce simp: has_overlap_def overlap_def)
+            using a_disjoint by (auto simp: has_overlap_def overlap_def)
         qed
       next
         case False
@@ -251,7 +249,7 @@
           by (fastforce simp: overlap_def)
         then show ?thesis
           unfolding search_eval search_r
-          using a_disjoint by (fastforce simp: has_overlap_def overlap_def)
+          using a_disjoint by (auto simp: has_overlap_def overlap_def)
       qed
     qed
   qed