tuned
authornipkow
Wed Jan 25 18:26:35 2017 +0100 (2017-01-25)
changeset 64947f6ad52152040
parent 64946 03b5f4e7f4a6
child 64948 e655d965307c
tuned
src/HOL/Data_Structures/RBT_Set.thy
     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" |