src/HOL/Data_Structures/RBT_Set.thy
changeset 64947 f6ad52152040
parent 64242 93c6f0da5c70
child 64950 10b8d31634cc
     1.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Tue Jan 24 22:29:44 2017 +0100
     1.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Wed Jan 25 18:26:35 2017 +0100
     1.3 @@ -103,7 +103,7 @@
     1.4  fun invc :: "'a rbt \<Rightarrow> bool" where
     1.5  "invc Leaf = True" |
     1.6  "invc (Node c l a r) =
     1.7 -  (invc l \<and> invc r \<and> (c = Black \<or> color l = Black \<and> color r = Black))"
     1.8 +  (invc l \<and> invc r \<and> (c = Red \<longrightarrow> color l = Black \<and> color r = Black))"
     1.9  
    1.10  fun invc_sons :: "'a rbt \<Rightarrow> bool" \<comment> \<open>Weaker version\<close> where
    1.11  "invc_sons Leaf = True" |