# HG changeset patch
# User nipkow
# Date 1730832735 -3600
# Node ID db791a3b098f2aa66a2649fabaa0608699cffc25
# Parent  31f9e5ada55054e2f0577f3d942d2af1d1a2d7c8
added missing definitions

diff -r 31f9e5ada550 -r db791a3b098f src/HOL/Data_Structures/Set2_Join_RBT.thy
--- a/src/HOL/Data_Structures/Set2_Join_RBT.thy	Mon Nov 04 22:36:42 2024 +0100
+++ b/src/HOL/Data_Structures/Set2_Join_RBT.thy	Tue Nov 05 19:52:15 2024 +0100
@@ -227,6 +227,7 @@
 where join = join and inv = "\<lambda>t. invc t \<and> invh t"
 defines insert_rbt = RBT.insert and delete_rbt = RBT.delete and split_rbt = RBT.split
 and join2_rbt = RBT.join2 and split_min_rbt = RBT.split_min
+and inter_rbt = RBT.inter and union_rbt = RBT.union and diff_rbt = RBT.diff 
 proof (standard, goal_cases)
   case 1 show ?case by (rule set_join)
 next