--- a/src/HOL/Data_Structures/Tree23_Set.thy Sun Nov 08 21:27:08 2020 +0100
+++ b/src/HOL/Data_Structures/Tree23_Set.thy Tue Nov 10 17:42:41 2020 +0100
@@ -114,7 +114,7 @@
"split_min (Node3 l a m b r) = (let (x,l') = split_min l in (x, node31 l' a m b r))"
text \<open>In the base cases of \<open>split_min\<close> and \<open>del\<close> it is enough to check if one subtree is a \<open>Leaf\<close>,
-in which case balancedness implies that so are the others. Exercise.\<close>
+in which case completeness implies that so are the others. Exercise.\<close>
fun del :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a upD" where
"del x Leaf = TD Leaf" |
@@ -203,7 +203,7 @@
by(simp add: delete_def inorder_del)
-subsection \<open>Balancedness\<close>
+subsection \<open>Completeness\<close>
subsubsection "Proofs for insert"
@@ -225,7 +225,7 @@
by (induct t) (auto split!: if_split upI.split) (* 15 secs in 2015 *)
text\<open>Now an alternative proof (by Brian Huffman) that runs faster because
-two properties (balance and height) are combined in one predicate.\<close>
+two properties (completeness and height) are combined in one predicate.\<close>
inductive full :: "nat \<Rightarrow> 'a tree23 \<Rightarrow> bool" where
"full 0 Leaf" |