removed contribution by Daniel Stuewe, too detailed.
authornipkow
Fri Jan 27 12:32:49 2017 +0100 (2017-01-27)
changeset 64951140addd19343
parent 64950 10b8d31634cc
child 64952 f11e974b47e0
removed contribution by Daniel Stuewe, too detailed.
src/HOL/Data_Structures/RBT_Set.thy
     1.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Thu Jan 26 17:51:13 2017 +0100
     1.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Fri Jan 27 12:32:49 2017 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -(* Author: Tobias Nipkow, Daniel Stüwe *)
     1.5 +(* Author: Tobias Nipkow *)
     1.6  
     1.7  section \<open>Red-Black Tree Implementation of Sets\<close>
     1.8  
     1.9 @@ -99,7 +99,7 @@
    1.10  
    1.11  fun bheight :: "'a rbt \<Rightarrow> nat" where
    1.12  "bheight Leaf = 0" |
    1.13 -"bheight (Node c l x r) = (if c = Black then Suc(bheight l) else bheight l)"
    1.14 +"bheight (Node c l x r) = (if c = Black then bheight l + 1 else bheight l)"
    1.15  
    1.16  fun invc :: "'a rbt \<Rightarrow> bool" where
    1.17  "invc Leaf = True" |