diff -r ed5b907bbf50 -r 831f17da1aab src/HOL/Data_Structures/Braun_Tree.thy
--- a/src/HOL/Data_Structures/Braun_Tree.thy	Sun Nov 08 21:27:08 2020 +0100
+++ b/src/HOL/Data_Structures/Braun_Tree.thy	Tue Nov 10 17:42:41 2020 +0100
@@ -30,13 +30,13 @@
   thus ?case using Node.prems(1,2) Node.IH by auto
 qed
 
-text \<open>Braun trees are balanced:\<close>
+text \<open>Braun trees are almost complete:\<close>
 
-lemma balanced_if_braun: "braun t \<Longrightarrow> balanced t"
+lemma acomplete_if_braun: "braun t \<Longrightarrow> acomplete t"
 proof(induction t)
-  case Leaf show ?case by (simp add: balanced_def)
+  case Leaf show ?case by (simp add: acomplete_def)
 next
-  case (Node l x r) thus ?case using balanced_Node_if_wbal2 by force
+  case (Node l x r) thus ?case using acomplete_Node_if_wbal2 by force
 qed
 
 subsection \<open>Numbering Nodes\<close>