# HG changeset patch
# User nipkow
# Date 1485365195 -3600
# Node ID f6ad52152040abdbf76c6c9bc6ad87cc49e0a5fa
# Parent  03b5f4e7f4a624f61aad5c4cd87d2bb3c2a05762
tuned

diff -r 03b5f4e7f4a6 -r f6ad52152040 src/HOL/Data_Structures/RBT_Set.thy
--- a/src/HOL/Data_Structures/RBT_Set.thy	Tue Jan 24 22:29:44 2017 +0100
+++ b/src/HOL/Data_Structures/RBT_Set.thy	Wed Jan 25 18:26:35 2017 +0100
@@ -103,7 +103,7 @@
 fun invc :: "'a rbt \<Rightarrow> bool" where
 "invc Leaf = True" |
 "invc (Node c l a r) =
-  (invc l \<and> invc r \<and> (c = Black \<or> color l = Black \<and> color r = Black))"
+  (invc l \<and> invc r \<and> (c = Red \<longrightarrow> color l = Black \<and> color r = Black))"
 
 fun invc_sons :: "'a rbt \<Rightarrow> bool" \<comment> \<open>Weaker version\<close> where
 "invc_sons Leaf = True" |