# HG changeset patch
# User nipkow
# Date 1580750579 -3600
# Node ID 63b2789259e7b09789788289746f0b155e5be4dc
# Parent  c26de1bd7b0037cf6c630ad6d1819c70ff0d31de
tuned

diff -r c26de1bd7b00 -r 63b2789259e7 src/HOL/Data_Structures/Interval_Tree.thy
--- a/src/HOL/Data_Structures/Interval_Tree.thy	Mon Feb 03 16:49:44 2020 +0100
+++ b/src/HOL/Data_Structures/Interval_Tree.thy	Mon Feb 03 18:22:59 2020 +0100
@@ -40,21 +40,21 @@
 
 instantiation ivl :: (linorder) linorder begin
 
-definition int_less: "(x < y) = (low x < low y | (low x = low y \<and> high x < high y))"
-definition int_less_eq: "(x \<le> y) = (low x < low y | (low x = low y \<and> high x \<le> high y))"
+definition ivl_less: "(x < y) = (low x < low y | (low x = low y \<and> high x < high y))"
+definition ivl_less_eq: "(x \<le> y) = (low x < low y | (low x = low y \<and> high x \<le> high y))"
 
 instance proof
   fix x y z :: "'a ivl"
   show a: "(x < y) = (x \<le> y \<and> \<not> y \<le> x)"
-    using int_less int_less_eq by force
+    using ivl_less ivl_less_eq by force
   show b: "x \<le> x"
-    by (simp add: int_less_eq)
+    by (simp add: ivl_less_eq)
   show c: "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
-    by (smt int_less_eq dual_order.trans less_trans)
+    by (smt ivl_less_eq dual_order.trans less_trans)
   show d: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
-    using int_less_eq a ivl_inj int_less by fastforce
+    using ivl_less_eq a ivl_inj ivl_less by fastforce
   show e: "x \<le> y \<or> y \<le> x"
-    by (meson int_less_eq leI not_less_iff_gr_or_eq)
+    by (meson ivl_less_eq leI not_less_iff_gr_or_eq)
 qed end
 
 
@@ -234,7 +234,7 @@
             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 int_less)
+              using Node(4) by(fastforce simp: sorted_wrt_append ivl_less)
             then show ?thesis
               using False by (auto simp: overlap_def)
           qed