--- 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" |