Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed contribution by Daniel Stuewe, too detailed.
authornipkow
Fri, 27 Jan 2017 12:32:49 +0100
changeset 64951 140addd19343
parent 64950 10b8d31634cc
child 64952 f11e974b47e0
removed contribution by Daniel Stuewe, too detailed.
src/HOL/Data_Structures/RBT_Set.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Data_Structures/RBT_Set.thy	Thu Jan 26 17:51:13 2017 +0100
+++ b/src/HOL/Data_Structures/RBT_Set.thy	Fri Jan 27 12:32:49 2017 +0100
@@ -1,4 +1,4 @@
-(* Author: Tobias Nipkow, Daniel Stüwe *)
+(* Author: Tobias Nipkow *)
 
 section \<open>Red-Black Tree Implementation of Sets\<close>
 
@@ -99,7 +99,7 @@
 
 fun bheight :: "'a rbt \<Rightarrow> nat" where
 "bheight Leaf = 0" |
-"bheight (Node c l x r) = (if c = Black then Suc(bheight l) else bheight l)"
+"bheight (Node c l x r) = (if c = Black then bheight l + 1 else bheight l)"
 
 fun invc :: "'a rbt \<Rightarrow> bool" where
 "invc Leaf = True" |
isabelle