# HG changeset patch
# User nipkow
# Date 1607445643 -3600
# Node ID f0fa51227a235f95499550487677b2a8de5cf2b6
# Parent  4cb480334f488d3043ce3cc92123b4ce7b0db6be
tuned

diff -r 4cb480334f48 -r f0fa51227a23 src/HOL/Data_Structures/RBT_Set.thy
--- a/src/HOL/Data_Structures/RBT_Set.thy	Mon Dec 07 22:28:41 2020 +0100
+++ b/src/HOL/Data_Structures/RBT_Set.thy	Tue Dec 08 17:40:43 2020 +0100
@@ -265,13 +265,13 @@
 
 lemma inv_del: "\<lbrakk> invh t; invc t \<rbrakk> \<Longrightarrow>
    invh (del x t) \<and>
-   (color t = Red \<and> bheight (del x t) = bheight t \<and> invc (del x t) \<or>
-    color t = Black \<and> bheight (del x t) = bheight t - 1 \<and> invc2 (del x t))"
+   (color t = Red \<longrightarrow> bheight (del x t) = bheight t \<and> invc (del x t)) \<and>
+   (color t = Black \<longrightarrow> bheight (del x t) = bheight t - 1 \<and> invc2 (del x t))"
 by(induct x t rule: del.induct)
   (auto simp: inv_baldL inv_baldR inv_join dest!: neq_LeafD)
 
 theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete x t)"
-by (metis delete_def rbt_def color_paint_Black inv_del invc2I invh_paint)
+by (metis delete_def rbt_def color_paint_Black inv_del invh_paint)
 
 text \<open>Overall correctness:\<close>