--- a/src/HOL/Data_Structures/Set2_Join_RBT.thy Tue Sep 24 17:36:14 2019 +0200
+++ b/src/HOL/Data_Structures/Set2_Join_RBT.thy Wed Sep 25 17:22:57 2019 +0200
@@ -179,7 +179,7 @@
by(cases "(l,a,r)" rule: baliR.cases) (auto simp: ball_Un)
lemma bst_joinL:
- "\<lbrakk>bst (Node l a n r); bheight l \<le> bheight r\<rbrakk>
+ "\<lbrakk>bst (Node l (a, n) r); bheight l \<le> bheight r\<rbrakk>
\<Longrightarrow> bst (joinL l a r)"
proof(induction l a r rule: joinL.induct)
case (1 l a r)
@@ -202,7 +202,7 @@
by(cases t) auto
lemma bst_join:
- "bst (Node l a n r) \<Longrightarrow> bst (join l a r)"
+ "bst (Node l (a, n) r) \<Longrightarrow> bst (join l a r)"
by(auto simp: bst_paint bst_joinL bst_joinR join_def)
lemma inv_join: "\<lbrakk> invc l; invh l; invc r; invh r \<rbrakk> \<Longrightarrow> invc(join l x r) \<and> invh(join l x r)"