# HG changeset patch
# User nipkow
# Date 1618840514 -7200
# Node ID c1f8aaa13ee3c6ef0d9c54f0cef9028e242ffd1c
# Parent  1aa9ef7a3eafd7bf2ae433bd020836c33f03b16e
tuned

diff -r 1aa9ef7a3eaf -r c1f8aaa13ee3 src/HOL/Data_Structures/RBT_Set2.thy
--- a/src/HOL/Data_Structures/RBT_Set2.thy	Sat Apr 17 19:47:08 2021 +0200
+++ b/src/HOL/Data_Structures/RBT_Set2.thy	Mon Apr 19 15:55:14 2021 +0200
@@ -94,13 +94,19 @@
   proof cases
     assume "x < a"
     show ?thesis
-    proof cases (* For readability; could be automated more: *)
-      assume *: "l \<noteq> Leaf \<and> color l = Black"
-      hence "bheight l > 0" using neq_LeafD[of l] by auto
-      thus ?thesis using \<open>x < a\<close> "2.IH"(1) "2.prems" inv_baldL[of "del x l"] * by(auto)
+    proof cases (* For readability; is automated more (below) *)
+      assume "l = Leaf" thus ?thesis using \<open>x < a\<close> "2.prems" by(auto)
     next
-      assume "\<not>(l \<noteq> Leaf \<and> color l = Black)"
-      thus ?thesis using \<open>x < a\<close> "2.prems" "2.IH"(1) by(auto)
+      assume l: "l \<noteq> Leaf"
+      show ?thesis
+      proof (cases "color l")
+        assume *: "color l = Black"
+        hence "bheight l > 0" using l neq_LeafD[of l] by auto
+        thus ?thesis using \<open>x < a\<close> "2.IH"(1) "2.prems" inv_baldL[of "del x l"] * l by(auto)
+      next
+        assume "color l = Red"
+        thus ?thesis using \<open>x < a\<close> "2.prems" "2.IH"(1) by(auto)
+      qed
     qed
   next (* more automation: *)
     assume "\<not> x < a"