# HG changeset patch
# User nipkow
# Date 1606415248 -3600
# Node ID 7b918b9f0122222b75bd80a20d92f4331430bd6e
# Parent  bfd1022cd9479da96b08c1c4f1eef73331589638
tuned

diff -r bfd1022cd947 -r 7b918b9f0122 src/HOL/Data_Structures/Interval_Tree.thy
--- a/src/HOL/Data_Structures/Interval_Tree.thy	Thu Nov 26 14:53:38 2020 +0100
+++ b/src/HOL/Data_Structures/Interval_Tree.thy	Thu Nov 26 19:27:28 2020 +0100
@@ -265,10 +265,13 @@
   fixes has_overlap :: "'t \<Rightarrow> 'a::linorder ivl \<Rightarrow> bool"
   assumes set_overlap: "invar s \<Longrightarrow> has_overlap s x = Interval_Tree.has_overlap (set s) x"
 
+fun invar :: "('a::{linorder,order_bot}) ivl_tree \<Rightarrow> bool" where
+"invar t = (inv_max_hi t \<and> sorted(inorder t))"
+
 interpretation S: Interval_Set
   where empty = Leaf and insert = insert and delete = delete
   and has_overlap = search and isin = isin and set = set_tree
-  and invar = "\<lambda>t. inv_max_hi t \<and> sorted (inorder t)"
+  and invar = invar
 proof (standard, goal_cases)
   case 1
   then show ?case by auto